--- 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