| changeset 54444 | a2290f36d1d6 |
| parent 54442 | c39972ddd672 |
| child 54512 | 7a92ed889da4 |
--- a/src/Pure/General/bytes.scala Sat Nov 16 12:29:10 2013 +0100 +++ b/src/Pure/General/bytes.scala Sat Nov 16 12:41:16 2013 +0100 @@ -91,7 +91,8 @@ def sha1_digest: SHA1.Digest = SHA1.digest(bytes) - override def toString: String = new String(bytes, offset, length, UTF8.charset) + override def toString: String = + UTF8.decode_chars(s => s, bytes, offset, offset + length).toString def isEmpty: Boolean = length == 0