Format JSON numbers correctly regardless of locale.

Use decimal point "." instead of ",", even if the execution locale is
Norwegian.