src/Pure/ML/ml_heap.scala

--- a/src/Pure/ML/ml_heap.scala	Sun Nov 12 12:33:22 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala	Sun Nov 12 12:34:04 2023 +0100
@@ -21,7 +21,7 @@
     if (heap.is_file) {
       val l = sha1_prefix.length
       val m = l + SHA1.digest_length
-      val n = heap.file.length
+      val n = File.size(heap)
       val bs = Bytes.read_file(heap, offset = n - m)
       if (bs.length == m) {
         val s = bs.text