awk (gawk) stampa i numeri decimali con la virgola invece che con il punto

[Mattia <mattia.list@gmail.com>]

Ciao a tutti,
mi rendo conto che l'argomento è una sciocchezza però è da più di
un'ora che ci sbatto la testa e vorrei capire se è un problema solo mio.

Venendo al dunque: se lancio questo comando:

echo 10 |LC_ALL=it_IT.UTF-8 gawk '{print $1/3}'

ottengo 3,33333. Se invece lancio

echo 10 |LC_ALL=C gawk '{print $1/3}'

ottengo 3.33333, cioè col punto invece che con la virgola.
Evidentemente gawk tiene conto del locale per stampare il carattere
che separa i decimali.
Non sarebbe meglio avere il punto come separatore per ogni locale visto
che nella documentazione di gawk si usa sempre il punto?
Come mai altri programmi tipo bc usano il punto?
Non c'è un comportamento standard per tutti?

ciao