fix numeric locale

In some locales (e.g. de_DE) floats have commas instead of
dots, but JSON requires dots.
See:
  https://github.com/open-source-parsers/jsoncpp/pull/9
  https://github.com/open-source-parsers/jsoncpp/pull/3

src/lib_json/json_tool.h

@@ -68,6 +68,20 @@ static inline void uintToString(LargestUInt value, char *&current) {
   } while (value != 0);
 }
 
+/** Change ',' to '.' everywhere in buffer.
+ *
+ * We had a sophisticated way, but it did not work in WinCE.
+ * @see https://github.com/open-source-parsers/jsoncpp/pull/9
+ */
+static inline void fixNumericLocale(char* begin, char* end) {
+  while (begin < end) {
+    if (*begin == ',') {
+      *begin = '.';
+    }
+    ++begin;
+  }
+}
+
 } // namespace Json {
 
 #endif // LIB_JSONCPP_JSON_TOOL_H_INCLUDED

src/lib_json/json_writer.cpp

@@ -77,7 +77,7 @@ std::string valueToString(double value) {
 #else
   snprintf(buffer, sizeof(buffer), "%.16g", value);
 #endif
-
+  fixNumericLocale(buffer, buffer + strlen(buffer));
   return buffer;
 }