changeset 75709 | a068fb7346ef |
parent 75620 | 44815dc2b8f9 |
child 76236 | 03dd2f19f1d7 |
--- a/src/Pure/General/bytes.scala Wed Jul 27 12:49:31 2022 +0200 +++ b/src/Pure/General/bytes.scala Wed Jul 27 13:13:59 2022 +0200 @@ -57,12 +57,11 @@ val buf = new Array[Byte](8192) var m = 0 - var cont = true - while (cont) { + while ({ m = stream.read(buf, 0, buf.length min (limit - out.size)) if (m != -1) out.write(buf, 0, m) - cont = (m != -1 && limit > out.size) - } + m != -1 && limit > out.size + }) () new Bytes(out.toByteArray, 0, out.size) }