format is "%9d.%09d.%03d". This is not properly a flating point number, but
counting 9 digits is already heavy, I'd better not have a 12-digit field
(which, btw, will be wrongly converted by 32-bit parsers).

This comes from a similar change by Peter Jansweijer from nikhef,
for absolute-calibration work.
Signed-off-by: Alessandro Rubini <rubini@gnudd.com>