# HG changeset patch
# User wenzelm
# Date 1720179515 -7200
# Node ID 6a58d706cfb26d129ae6988bd9a8a9695c60e3fe
# Parent  11ca26978dd4ea5b3bcc270a1b8f7a2b7e807d39
tuned;

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