--- 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 = {