src/Pure/General/bytes.scala
changeset 75382 81673c441ce3
parent 73576 b50f8cc8c08e
child 75393 87ebf5a50283
--- 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)
     }