objfloat: Try to achieve the same float printing format as CPython does.

Test usecase I used is print(time.time()) and print(time.time() - time.time()).
On Linux/Glibc they now give the same output as CPython 3.3. Specifically,
time.time() gives non-exponential output with 7 decimal digits, and subtraction
gives exponential output e-06/e-07.

py/objfloat.c

@@ -30,7 +30,7 @@ STATIC void float_print(void (*print)(void *env, const char *fmt, ...), void *en
     }
 #else
     char buf[32];
-    sprintf(buf, "%.8g", (double) o->value);
+    sprintf(buf, "%.17g", (double) o->value);
     print(env, buf);
     if (strchr(buf, '.') == NULL) {
         // Python floats always have decimal point