--- a/src/Pure/Tools/build_job.scala Mon Feb 06 12:58:45 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Feb 06 14:54:15 2023 +0100
@@ -570,7 +570,7 @@
else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
}
- def join: (Process_Result, String) = {
+ def join: (Process_Result, SHA1.Shasum) = {
val result1 = future_result.join
val was_timeout =
@@ -585,17 +585,11 @@
else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
else result1
- val heap_digest =
+ val heap_shasum =
if (result2.ok && do_store && store.output_heap(session_name).is_file) {
- Some(ML_Heap.write_digest(store.output_heap(session_name)))
+ SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
}
- else None
-
- val heap_shasum =
- heap_digest match {
- case None => ""
- case Some(digest) => SHA1.shasum(digest, session_name) + "\n"
- }
+ else SHA1.no_shasum
(result2, heap_shasum)
}