author | wenzelm |
Sat, 10 Apr 2021 20:22:07 +0200 | |
changeset 73554 | c973b5300025 |
parent 73553 | b35ef8162807 |
child 73555 | 92783562ab78 |
child 73556 | 192bcee4f8b8 |
--- 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)