(that is, these numbers are converted to doubles by a local OS strtod,
and on different systems they get different values)