changeset 78182 | 31835adf148a |
parent 78181 | c2fbe48e9df4 |
child 78184 | 4309bcc8f28b |
--- a/src/Pure/Thy/store.scala Tue Jun 20 16:48:47 2023 +0200 +++ b/src/Pure/Thy/store.scala Tue Jun 20 18:23:17 2023 +0200 @@ -230,7 +230,7 @@ def find_heap_shasum(name: String): SHA1.Shasum = (for { path <- find_heap(name) - digest <- ML_Heap.read_digest(path) + digest <- ML_Heap.read_file_digest(path) } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum) def the_heap(name: String): Path =