problème d'arrondi avec gawk

Bonjour, j'essaye la commande suivante :

Code:

---

1 2	echo 0,019 | awk '{printf("%f\n",$1);}'

---

qui me renvoie 0,000.
c'est gawk qui est installé sur ma machine. Sur une autre machine avec mawk, pas de souci.

Ca ne fait ça qu'avec 0, car si j'essaye

Code:

---

1 2	echo 1,019 | awk '{printf("%f\n",$1);}'

---

gawk me renvoie bien 1,019

Quelqu'un peut il m'expliquer ?

Merci !

Cela peut il etre lié à la gestion du séparateur des entiers et decimal ?
la virgule "," ou le point "."
Avez vous fait le meme test avec "0.0019" ?