diff -r e06e899b78d0 -r 9da65bc75610 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sun Sep 04 15:44:20 2016 +0200 +++ b/src/Pure/General/bytes.scala Sun Sep 04 17:38:22 2016 +0200 @@ -25,6 +25,8 @@ } } + def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length) + def apply(a: Array[Byte], offset: Int, length: Int): Bytes = if (length == 0) empty else {