Re: [PATCH] 4511638: Double.toString(double) sometimes produces incorrect results