# HG changeset patch
# User wenzelm
# Date 1618078927 -7200
# Node ID c973b530002512437cc79109b10d1ab54d4cbd51
# Parent  b35ef81628071800edf6e87c67a48732b0b8c2de
tuned;

diff -r b35ef8162807 -r c973b5300025 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)