diff -r 3d37b2957a3e -r c39972ddd672 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Thu Nov 14 17:39:32 2013 +0100 +++ b/src/Pure/General/bytes.scala Fri Nov 15 19:31:10 2013 +0100 @@ -20,11 +20,19 @@ val str = s.toString if (str.isEmpty) empty else { - val bytes = str.getBytes(UTF8.charset) - new Bytes(bytes, 0, bytes.length) + val b = str.getBytes(UTF8.charset) + new Bytes(b, 0, b.length) } } + def apply(a: Array[Byte], offset: Int, length: Int): Bytes = + if (length == 0) empty + else { + val b = new Array[Byte](length) + java.lang.System.arraycopy(a, offset, b, 0, length) + new Bytes(b, 0, b.length) + } + /* read */