tuned;
authorwenzelm
Sat, 10 Apr 2021 20:22:07 +0200
changeset 73554 c973b5300025
parent 73553 b35ef8162807
child 73555 92783562ab78
child 73556 192bcee4f8b8
tuned;
src/Pure/General/bytes.scala
--- 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)