src/Pure/General/bytes.scala
changeset 73554 c973b5300025
parent 73414 7411d71b9fb8
child 73559 22b5ecb53dd9
--- a/src/Pure/General/bytes.scala	Sat Apr 10 19:45:51 2021 +0200
+++ b/src/Pure/General/bytes.scala	Sat Apr 10 20:22:07 2021 +0200
@@ -59,7 +59,7 @@
       var m = 0
 
       do {
-        m = stream.read(buf, 0, buf.size min (limit - out.size))
+        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)