# HG changeset patch
# User wenzelm
# Date 1675847910 -3600
# Node ID dce91dab1728eec2253ffdc3898c32da1049219b
# Parent  0c073854e6cea441c3b5c66c28b5d52a4c847ec7
clarified signature;

diff -r 0c073854e6ce -r dce91dab1728 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/Pure/Tools/build.scala	Wed Feb 08 10:18:30 2023 +0100
@@ -315,7 +315,13 @@
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
-            val (process_result, output_heap) = job.join
+            val process_result = job.join
+
+            val output_heap =
+              if (process_result.ok && job.do_store && store.output_heap(session_name).is_file) {
+                SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
+              }
+              else SHA1.no_shasum
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail = {
diff -r 0c073854e6ce -r dce91dab1728 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/Pure/Tools/build_job.scala	Wed Feb 08 10:18:30 2023 +0100
@@ -238,7 +238,7 @@
 class Build_Job(progress: Progress,
   session_background: Sessions.Background,
   store: Sessions.Store,
-  do_store: Boolean,
+  val do_store: Boolean,
   log: Logger,
   session_setup: (String, Session) => Unit,
   val numa_node: Option[Int],
@@ -570,8 +570,8 @@
     else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
   }
 
-  def join: (Process_Result, SHA1.Shasum) = {
-    val result1 = future_result.join
+  def join: Process_Result = {
+    val result = future_result.join
 
     val was_timeout =
       timeout_request match {
@@ -579,18 +579,9 @@
         case Some(request) => !request.cancel()
       }
 
-    val result2 =
-      if (result1.ok) result1
-      else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc
-      else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
-      else result1
-
-    val heap_shasum =
-      if (result2.ok && do_store && store.output_heap(session_name).is_file) {
-        SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
-      }
-      else SHA1.no_shasum
-
-    (result2, heap_shasum)
+    if (result.ok) result
+    else if (was_timeout) result.error(Output.error_message_text("Timeout")).timeout_rc
+    else if (result.interrupted) result.error(Output.error_message_text("Interrupt"))
+    else result
   }
 }