# 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)