src/Pure/General/bytes.scala
changeset 73414 7411d71b9fb8
parent 73024 337e1b135d2f
child 73554 c973b5300025
--- a/src/Pure/General/bytes.scala	Thu Mar 11 20:30:56 2021 +0100
+++ b/src/Pure/General/bytes.scala	Fri Mar 12 19:42:18 2021 +0100
@@ -53,7 +53,8 @@
   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
     if (limit == 0) empty
     else {
-      val out = new ByteArrayOutputStream(if (limit == Integer.MAX_VALUE) hint else limit)
+      val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
+      val out = new ByteArrayOutputStream(out_size)
       val buf = new Array[Byte](8192)
       var m = 0