# HG changeset patch
# User wenzelm
# Date 1673811507 -3600
# Node ID 11c0747a87fc477e4df0820f25d186c767d351bc
# Parent  6a078c80eab6d93255f922b71d8b20ddfe194169
tuned;

diff -r 6a078c80eab6 -r 11c0747a87fc src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sun Jan 15 20:20:59 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala	Sun Jan 15 20:38:27 2023 +0100
@@ -48,11 +48,9 @@
   }
 
   def write_digest(heap: Path): String =
-    read_digest(heap) match {
-      case None =>
-        val s = SHA1.digest(heap).toString
-        File.append(heap, sha1_prefix + s)
-        s
-      case Some(s) => s
+    read_digest(heap) getOrElse {
+      val s = SHA1.digest(heap).toString
+      File.append(heap, sha1_prefix + s)
+      s
     }
 }
diff -r 6a078c80eab6 -r 11c0747a87fc src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Jan 15 20:20:59 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sun Jan 15 20:38:27 2023 +0100
@@ -591,8 +591,9 @@
       else result1
 
     val heap_digest =
-      if (result2.ok && do_store && store.output_heap(session_name).is_file)
+      if (result2.ok && do_store && store.output_heap(session_name).is_file) {
         Some(ML_Heap.write_digest(store.output_heap(session_name)))
+      }
       else None
 
     (result2, heap_digest)