# HG changeset patch
# User wenzelm
# Date 1688135163 -7200
# Node ID 13863eaf372a4ce9996bd0fd8f7a34e423bbf8f3
# Parent  1a12e6246212846acd310f7c0284a6abc37f4a38
more robust database setup;

diff -r 1a12e6246212 -r 13863eaf372a src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Jun 30 16:04:53 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jun 30 16:26:03 2023 +0200
@@ -80,15 +80,6 @@
           }
       }
 
-    using_option(store.maybe_open_build_database()) { db =>
-      val shared_db = db.is_postgresql
-      Data.transaction_lock(db, create = true) {
-        Data.clean_build(db)
-        if (shared_db) Store.Data.tables.lock(db, create = true)
-      }
-      Data.vacuum(db, more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty)
-    }
-
     val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
 
     new Context(store, build_deps, sessions, ordering, ml_platform, hostname, numa_nodes,
@@ -826,7 +817,18 @@
     catch { case exn: Throwable => close(); throw exn }
 
   private val _build_database: Option[SQL.Database] =
-    try { store.maybe_open_build_database() }
+    try {
+      for (db <- store.maybe_open_build_database()) yield {
+        val shared_db = db.is_postgresql
+        Build_Process.Data.transaction_lock(db, create = true) {
+          Build_Process.Data.clean_build(db)
+          if (shared_db) Store.Data.tables.lock(db, create = true)
+        }
+        Build_Process.Data.vacuum(db,
+          more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty)
+        db
+      }
+    }
     catch { case exn: Throwable => close(); throw exn }
 
   private val _host_database: Option[SQL.Database] =