rounding bug (?) in gawk 3.1.2

[luca de filippis]

hello
maybe i found a bug that is not in know bug section at info gawk.

the code
awk 'BEGIN { for (i=0; i<=9; i++)
     printf "%2i %5.2f \n", i, 0.01+i/1000 }'

gives
 0  0.01
 1  0.01
 2  0.01
 3  0.01
 4  0.01
 5  0.01
 6  0.02
 7  0.02
 8  0.02
 9  0.02

which is wrong: value on row number 5 has to be 0.02

i use GNU Awk 3.1.2 on linux mdk 9.2 for x86

regards,
luca de filippis