# HG changeset patch
# User wenzelm
# Date 1615574538 -3600
# Node ID 7411d71b9fb80c002e9c9b8a00e0d7f2a887ff8b
# Parent  56c0a793cd8b8e7bda779ae3a57840f2b9070ac4
more robust;

diff -r 56c0a793cd8b -r 7411d71b9fb8 src/Pure/General/bytes.scala
--- 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