| changeset 62527 | aae9a2a855e0 |
| parent 54444 | a2290f36d1d6 |
| child 64370 | 865b39487b5d |
--- a/src/Pure/System/utf8.scala Sun Mar 06 10:33:34 2016 +0100 +++ b/src/Pure/System/utf8.scala Sun Mar 06 11:59:35 2016 +0100 @@ -20,6 +20,8 @@ val charset: Charset = Charset.forName(charset_name) def codec(): Codec = Codec(charset) + def bytes(s: String): Array[Byte] = s.getBytes(charset) + /* permissive UTF-8 decoding */