author | wenzelm |
Sun, 16 Jun 2024 11:28:47 +0200 | |
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 = {