src/Pure/Thy/sessions.scala
changeset 73945 e61add9d5b5e
parent 73826 72900f34dbb3
child 74696 0554a5c4c191
--- a/src/Pure/Thy/sessions.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -1144,7 +1144,7 @@
   def read_heap_digest(heap: Path): Option[String] =
   {
     if (heap.is_file) {
-      using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file =>
+      using(FileChannel.open(heap.java_path, StandardOpenOption.READ))(file =>
       {
         val len = file.size
         val n = sha1_prefix.length + SHA1.digest_length