# HG changeset patch
# User wenzelm
# Date 1713262120 -7200
# Node ID d4d9a7887b2a39543b5b93869c04841d9f43e9aa
# Parent  c188068e41f19d2292542c100e0bc6a178d20fbb
tuned signature;

diff -r c188068e41f1 -r d4d9a7887b2a src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Tue Apr 16 11:39:02 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Apr 16 12:08:40 2024 +0200
@@ -23,6 +23,23 @@
 
   /* build session */
 
+  def store_heaps(
+    store: Store,
+    options: Options,
+    session: Store.Session,
+    database_server: Option[SQL.Database] = None,
+    server: SSH.Server = SSH.no_server,
+    progress: Progress = new Progress
+  ): Unit = {
+    using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
+      heaps_database =>
+        for (db <- database_server orElse heaps_database) {
+          val slice = Space.MiB(options.real("build_database_slice"))
+          ML_Heap.store(db, session, slice, cache = store.cache.compress, progress = progress)
+        }
+    }
+  }
+
   def start_session(
     build_context: Build.Context,
     session_context: Session_Context,
@@ -514,14 +531,8 @@
             case None => using(store.open_database(session_name, output = true))(write_info)
           }
 
-          using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
-            heaps_database =>
-              for (db <- database_server orElse heaps_database) {
-                val slice = Space.MiB(options.real("build_database_slice"))
-                ML_Heap.store(db, store_session, slice,
-                  cache = store.cache.compress, progress = progress)
-              }
-          }
+          store_heaps(store, options, store_session,
+            database_server = database_server, server = server, progress = progress)
 
           // messages
           process_result.err_lines.foreach(progress.echo(_))