objfloat.c

With 30-bit floats there aren't enough bits to faithfully print 7 decimal
digits, so reduce the precision to 6 digits.