index 8586650e879befb0813d937cbb30a9269c31aac9..adef3b6a261e55d120fc0ef40efa5a8557ec3ff2 100644 (file)
* print_double(x) has the same effect as printf("%g", x), but is intended
* to produce the same formatting across all platforms.
*/
-static void
+static inline void
print_double(double x)
{
#ifdef WIN32
index bf312549b4fc4cbef9c0430cb3b0293880256545..85ec13ec6ed0275d5cd5f52bb8d5bbc37c1fc6c0 100644 (file)
* print_double(x) has the same effect as printf("%g", x), but is intended
* to produce the same formatting across all platforms.
*/
-static void
+static inline void
print_double(double x)
{
#ifdef WIN32
index 9debc34e791dd0463a3b03b62a03159441c644e7..ebff9ca0359835fb53406bf6c481e5b1a8f5ab65 100644 (file)
* print_double(x) has the same effect as printf("%g", x), but is intended
* to produce the same formatting across all platforms.
*/
-static void
+static inline void
print_double(double x)
{
#ifdef WIN32