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