src/Pure/General/bytes.scala
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)
     }