--- a/src/Pure/Tools/build_process.scala Fri Jun 23 11:14:44 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Fri Jun 23 13:47:34 2023 +0200
@@ -905,6 +905,16 @@
val skipped = build_context.no_build
val cancelled = progress.stopped || !ancestor_results.forall(_.ok)
+ if (!skipped && !cancelled) {
+ val database = store.maybe_open_heaps_database()
+ try {
+ for (db <- database) {
+ ML_Heap.restore(db, store.output_heap(session_name), cache = store.cache.compress)
+ }
+ }
+ finally { database.foreach(_.close()) }
+ }
+
val result_name = (session_name, worker_uuid, build_uuid)
if (finished) {