# HG changeset patch
# User wenzelm
# Date 1713277660 -7200
# Node ID 370ebda8bd86c41c63cca9a977f20ca6f809183e
# Parent  47f671888a371da009b594bcb22f78f3336921a3
clarified signature;

diff -r 47f671888a37 -r 370ebda8bd86 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Tue Apr 16 15:14:55 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Apr 16 16:27:40 2024 +0200
@@ -31,12 +31,9 @@
     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)
-        }
+    store.maybe_using_heaps_database(database_server, server = server) { db =>
+      val slice = Space.MiB(options.real("build_database_slice"))
+      ML_Heap.store(db, session, slice, cache = store.cache.compress, progress = progress)
     }
   }
 
diff -r 47f671888a37 -r 370ebda8bd86 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Tue Apr 16 15:14:55 2024 +0200
+++ b/src/Pure/Build/store.scala	Tue Apr 16 16:27:40 2024 +0200
@@ -386,6 +386,15 @@
     else store.maybe_open_database_server(server = server, guard = build_cluster)
   }
 
+  def maybe_using_heaps_database[A](
+    database_server: Option[SQL.Database],
+    server: SSH.Server = SSH.no_server
+  )(f: SQL.Database => A): Option[A] = {
+    using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
+      heaps_database => (database_server orElse heaps_database).map(f)
+    }
+  }
+
   def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database =
     if (build_database_server || build_cluster) open_database_server(server = server)
     else SQLite.open_database(path, restrict = true)