changeset 71151 | 69a22ccd1817 |
parent 69454 | ef051edd4d10 |
child 71152 | f2d848a596d1 |
--- a/src/Pure/General/bytes.scala Fri Nov 22 15:26:08 2019 +0100 +++ b/src/Pure/General/bytes.scala Sat Nov 23 11:19:18 2019 +0100 @@ -66,7 +66,7 @@ } def read(file: JFile): Bytes = - using(new FileInputStream(file))(read_stream(_, file.length.toInt)) + using(new FileInputStream(file))(read_stream(_, limit = file.length.toInt)) def read(path: Path): Bytes = read(path.file)