gawk 3.1.6 and locale/decimal separator

[Hermann Peifer]

Gawk-3.1.6 doesn't seem to observe that locale de_DE.UTF-8  has the 
comma as decimal separator. This looks like a bug to me.

Regards, Hermann


address@hidden:~/tmp$ locale
LANG=de_DE.UTF-8
LC_CTYPE="de_DE.UTF-8"
LC_NUMERIC="de_DE.UTF-8"
LC_TIME="de_DE.UTF-8"
LC_COLLATE="de_DE.UTF-8"
LC_MONETARY="de_DE.UTF-8"
LC_MESSAGES="de_DE.UTF-8"
LC_PAPER="de_DE.UTF-8"
LC_NAME="de_DE.UTF-8"
LC_ADDRESS="de_DE.UTF-8"
LC_TELEPHONE="de_DE.UTF-8"
LC_MEASUREMENT="de_DE.UTF-8"
LC_IDENTIFICATION="de_DE.UTF-8"
LC_ALL=

address@hidden:~/tmp$ echo "12,345" | gawk-3.1.3/gawk '{print $1+2}'
14,345
address@hidden:~/tmp$ echo "12,345" | gawk-3.1.4/gawk '{print $1+2}'
14,345
address@hidden:~/tmp$ echo "12,345" | gawk-3.1.5/gawk '{print $1+2}'
14,345
address@hidden:~/tmp$ echo "12,345" | gawk-3.1.6/gawk '{print $1+2}'
14
address@hidden:~/tmp$