author | wenzelm |
Sat, 23 Nov 2019 11:19:18 +0100 | |
changeset 71151 | 69a22ccd1817 |
parent 71150 | 9e7d40d67258 |
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)