[patch #2] String.getBytes()

[Tom Tromey]

>> 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).

Per> It may be more correct to re-throw a non-checked exception, on
Per> the the theory that it is better to get an exception than
Per> silently do something different than the user asked for.

Then shouldn't we do the same thing in
UnicodeToBytes.getDefaultEncoder?

Hmm... the PrintStream docs say that it should use an ASCII encoding
when the encoder class is not available (we use 8859_1, which is
different, though perhaps only pedantically).

A footnote in the JCL book for String.getBytes (see p1638) says "If
the class for the converter cannot be loaded, an ASCII encoding is
used".  So I think the current code is ok.

Tom