Fix printing of floats.

print() would output 1.01700 instead of 1.17000 for a value value 1.17.