src/Pure/General/bytes.scala
changeset 78956 12abaffb0346
parent 78954 db9dba720ac7
child 79509 e82448aacf48
--- a/src/Pure/General/bytes.scala	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/Pure/General/bytes.scala	Sun Nov 12 12:26:08 2023 +0100
@@ -73,7 +73,7 @@
   def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
 
   def read_file(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
-    val length = File.space(path).bytes
+    val length = File.size(path)
     val start = offset.max(0L)
     val len = (length - start).max(0L).min(limit)
     if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)