# HG changeset patch
# User wenzelm
# Date 1718530127 -7200
# Node ID 224cdaaaf0cd8bfd93ab7a8463f30b462f0a400f
# Parent  2740dec064f903b5ecc7fe69280ed5da22b3f409
imitate internal policy of ByteArrayOutputStream: capacity is doubled after first push;

diff -r 2740dec064f9 -r 224cdaaaf0cd src/Pure/General/bytes.scala
--- 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 = {