Too many useless digits of precision

This is mostly to make the file a little shorter for humans to
read. But together with the previous commit, does same some
kb of data.