# HG changeset patch
# User wenzelm
# Date 1574504895 -3600
# Node ID f2d848a596d1f4f548ffa9d1e5a81abd6ff823e8
# Parent  69a22ccd181708406adad709a0c8c9c28026b1a2
more robust: file length can be invalid in odd situations;

diff -r 69a22ccd1817 -r f2d848a596d1 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Nov 23 11:19:18 2019 +0100
+++ b/src/Pure/General/bytes.scala	Sat Nov 23 11:28:15 2019 +0100
@@ -66,7 +66,11 @@
     }
 
   def read(file: JFile): Bytes =
-    using(new FileInputStream(file))(read_stream(_, limit = file.length.toInt))
+  {
+    val length = file.length
+    val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
+    using(new FileInputStream(file))(read_stream(_, limit = limit))
+  }
 
   def read(path: Path): Bytes = read(path.file)