Indeed, and that's exactly what the fix does:
sprintf(buf,"%.*"PRINTPIKEFLOAT"g", MAX_FLOAT_PREC_LEN, sp[-1].u.float_number); /* Ensure that a decimal point gets printed, since "g" removes it * completely if only zeroes would follow. Don't need to check for * an 'e', since if that is printed then "g" behaved like the "e" * format, and it always prints a '.' if the precision isn't * zero. */ if (!strchr (buf, '.')) strcat (buf, ".0");