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