diff -r 8b7497992301 -r 81673c441ce3 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Thu Mar 31 22:24:11 2022 +0200 +++ b/src/Pure/General/bytes.scala Thu Mar 31 22:40:34 2022 +0200 @@ -75,10 +75,12 @@ val buf = new Array[Byte](8192) var m = 0 - do { + var cont = true + while (cont) { m = stream.read(buf, 0, buf.length min (limit - out.size)) if (m != -1) out.write(buf, 0, m) - } while (m != -1 && limit > out.size) + cont = (m != -1 && limit > out.size) + } new Bytes(out.toByteArray, 0, out.size) }