fix misformatting of floats with leading zeros

[JelleZijlstra]

This is a bug in my previous code: it ended up turning "0.06" into "0.6".

The solution in this diff is a bit hacky, but it has the virtue of being correct, unlike the previous code.

It might be worth thinking about this part of the style some more: Should we even put underscores in the part of floats behind the decimal point? If so, should we count the groups from the end, like we do now, or from the beginning? (The difference between 0.12_345_678 and 0.123_456_78.)

[coveralls]

Pull Request Test Coverage Report for Build 644

• 1 of 1 (100.0%) changed or added relevant line in 1 file are covered.
• No unchanged relevant lines lost coverage.
• Overall coverage remained the same at 96.056%

---

Totals
Change from base Build 641:	0.0%
Covered Lines:	2679
Relevant Lines:	2789

---

💛 - Coveralls