gawk bug in reporting formatted numbers

[fuad badrieh]

Hello:

how come the following program

echo "0.2625e-6" | gawk 'BEGIN{OFMT="%9.3f"}{print $1*1e6}'

prints

0.262

and not 0.263?  The 25 should have been rounded to 3.

I am using gawk 3.0, patchlevel 0, on SunOS 5.8.



P.S
If I run the same thing through a C program it does print 0.263

#include <stdio.h>

int main() {
float x=0.2625e-6;
printf("%9.3f\n", x*1e6);
}

Thanks,
Fuad