printing big decimals

[Russ Cox]

running gawk-3.1.1.

gawk 'BEGIN{x=5*1024*1024*1024; printf("%d\n", x);}'

prints 5.36871e+09.  i think the implicit format for 
overflow of %d should be %.0f rather than whatever
it is.  that would preserve the illusion a bit longer.
i can't find mention of this in the man page.