gawk 3.1.3: $1 float interpretation

[Carlos Soria del Hoyo]

Hi,

I have some data file "foo", just 2 lines:

0.1
1.1

and the following simple awk-scipt "bar.awk":

// {print $1; print ($1 * 1000) }

Calling:

$ awk -f bar.awk foo

gives:

0.1
0
1.1
1000

It seems that the digits behind the decimal point are ignored. Former
gawk 3.1.0 gives:

0.1
100
1.1
1100

which is the right behaviour, I guess. A bug in gawk 3.1.3?

Greetings