src/Pure/General/bytes.scala
changeset 80383 224cdaaaf0cd
parent 80382 2740dec064f9
child 80384 061d672570f5
--- a/src/Pure/General/bytes.scala	Sat Jun 15 23:52:30 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sun Jun 16 11:28:47 2024 +0200
@@ -174,7 +174,7 @@
     private def buffer_check(): Unit =
       if (buffer_free() == 0) {
         chunks += buffer.toByteArray
-        buffer = new ByteArrayOutputStream
+        buffer = new ByteArrayOutputStream(chunk_size.toInt)
       }
 
     def += (b: Byte): Unit = {