Make real number encoding and decoding work under all locales