[patch #2] String.getBytes()

[Tom Tromey]

>>>>> "Bryce" == Bryce McKinlay <bryce@albatross.co.nz> writes:

Bryce> According to the JDK 1.2 docs, getBytes() isn't supposed to
Bryce> throw an UnsupportedEncodingException. I have confirmed this
Bryce> with JDK 1.2/javac

I agree the current implementation is wrong.  However, I'm not
entirely sure your patch is correct, either.  Eventually we'll compute
the `file.encoding' property from the user's locale information.  In
this case we might very well end up with a default encoding which is
not supported.

In this case I think we should just revert to using the 8859_1
encoding (for now; maybe later utf-8 would be a better choice).

However I think that Even my current change will be wrong, given that
none of the encoders will be pulled into the executable by default
without `-U' magic.

Tom