diff -r 11ca26978dd4 -r 6a58d706cfb2 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Fri Jul 05 13:36:49 2024 +0200 +++ b/src/Pure/General/bytes.scala Fri Jul 05 13:38:35 2024 +0200 @@ -38,11 +38,7 @@ /* main constructors */ - private def reuse_array(bytes: Array[Byte]): Bytes = - if (bytes.length <= chunk_size) new Bytes(None, bytes, 0L, bytes.length.toLong) - else apply(bytes) - - val empty: Bytes = reuse_array(new Array(0)) + val empty: Bytes = new Bytes(None, new Array(0), 0L, 0L) def raw(s: String): Bytes = if (s.isEmpty) empty