printf prints a decimal point when it shouldn't.
The following program shows the problem:

	main() { printf("%5.0f\n", 3.0/15000.0); }

This prints '   0.', but should print '    0' (according to the
man page and tradition).  When the value is really 0.0 it behaves
correctly.

I had a look at vfprintf, but decided to leave it to Torek
(I have a kludge, but there must be a better way).

	-- Lennart

------------------------------------------------------------------------------