# HG changeset patch
# User wenzelm
# Date 1720179661 -7200
# Node ID 4d142545b86b956b42f7912cb144e7c671928dc1
# Parent  6a58d706cfb26d129ae6988bd9a8a9695c60e3fe
tuned;

diff -r 6a58d706cfb2 -r 4d142545b86b src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Fri Jul 05 13:38:35 2024 +0200
+++ b/src/Pure/General/bytes.scala	Fri Jul 05 13:41:01 2024 +0200
@@ -240,7 +240,8 @@
       chunks = null
       buffer_list = null
       buffer = null
-      new Bytes(if (cs.isEmpty) None else Some(cs), b, 0L, size)
+      if (size == 0) empty
+      else new Bytes(if (cs.isEmpty) None else Some(cs), b, 0L, size)
     }
   }