Temporary patch for bug 1358192: printf("%f"...) sets fraction to zero.