# HG changeset patch
# User wenzelm
# Date 1708604835 -3600
# Node ID 2e1f75c870e39c9d4359993486cf67d1f0628e1c
# Parent  a2256e4a77bf80597a25183003bf22df5c11e0bb
more robust: make double-sure that heap digest is present;

diff -r a2256e4a77bf -r 2e1f75c870e3 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:24:26 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:27:15 2024 +0100
@@ -193,12 +193,7 @@
         uuid <- proper_string(Store.read_build_uuid(path, session.name))
       } yield Log_DB(uuid, Bytes.read(path))
 
-    val heap_digest =
-      for {
-        path <- session.heap
-        digest <- read_file_digest(path)
-      } yield digest
-
+    val heap_digest = session.heap.map(write_file_digest)
     val heap_size =
       session.heap match {
         case Some(heap) => File.size(heap) - sha1_prefix.length - SHA1.digest_length