diff -r 4f4a0c9d2d1a -r 3f2b1419f598 src/Pure/Tools/build_job.scala
--- 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
+  }
 }