# HG changeset patch # User wenzelm # Date 1574504358 -3600 # Node ID 69a22ccd181708406adad709a0c8c9c28026b1a2 # Parent 9e7d40d67258d0da477ae80a2b493ca8acaddc6a tuned; diff -r 9e7d40d67258 -r 69a22ccd1817 src/Pure/General/bytes.scala --- 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)