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            0 : 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            0 :         printf("%g", x);
      28              : #endif
      29            0 : }