Line data    Source code

       1             : /*
       2             :  * print_double(x) has the same effect as printf("%g", x), but is intended
       3             :  * to produce the same formatting across all platforms.
       4             :  */
       5             : static void
       6         112 : print_double(double x)
       7             : {
       8             : #ifdef WIN32
       9             :     /* Change Windows' 3-digit exponents to look like everyone else's */
      10             :     char        convert[128];
      11             :     int         vallen;
      12             : 
      13             :     sprintf(convert, "%g", x);
      14             :     vallen = strlen(convert);
      15             : 
      16             :     if (vallen >= 6 &&
      17             :         convert[vallen - 5] == 'e' &&
      18             :         convert[vallen - 3] == '0')
      19             :     {
      20             :         convert[vallen - 3] = convert[vallen - 2];
      21             :         convert[vallen - 2] = convert[vallen - 1];
      22             :         convert[vallen - 1] = '\0';
      23             :     }
      24             : 
      25             :     printf("%s", convert);
      26             : #else
      27         112 :     printf("%g", x);
      28             : #endif
      29         112 : }