java.lang.Double.parseDouble

[Tom Tromey]

>> static public double parseDouble(String s)
>> {
>> return doubleValueOf(s);
>> }

I'm finally checking in a variant of this.
Thanks.

Tom