Fix format for tiny double values in --help.

diff --git a/src/xbt/config.cpp b/src/xbt/config.cpp
index 76f7cbc..25feb08 100644 (file)
--- a/src/xbt/config.cpp
+++ b/src/xbt/config.cpp
@@ -210,7 +210,7 @@ public:
       this->update();
     } else {
       XBT_DEBUG("Do not override configuration variable '%s' with value '%s' because it was already set.",
-                get_key().c_str(), to_string(value).c_str());
+                get_key().c_str(), get_string_value().c_str());
     }
   }
 };
@@ -220,6 +220,12 @@ template <class T> std::string TypedConfigurationElement<T>::get_string_value()
   return to_string(content);
 }
 
+template <> std::string TypedConfigurationElement<double>::get_string_value() // override
+{
+  // don't want std::to_string which uses %f, and formats very small values as 0.000000
+  return xbt::string_printf("%g", content);
+}
+
 template <class T> void TypedConfigurationElement<T>::set_string_value(const char* value) // override
 {
   this->content = ConfigType<T>::parse(value);