Some locales (like German) use ',' as the decimal separator, so using
printf like functions to output a float value fails when the result
should always use '.'. Since there are only two distinct possibilities
we just write the string representation and be done with it.