--- a/src/Pure/Tools/build_job.scala Mon Feb 13 12:26:24 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Feb 13 12:36:49 2023 +0100
@@ -582,4 +582,12 @@
else if (result.interrupted) result.error(Output.error_message_text("Interrupt"))
else result
}
+
+ lazy val finish: SHA1.Shasum = {
+ require(is_finished, "Build job not finished: " + quote(session_name))
+ if (join.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
+ }
}