# HG changeset patch
# User wenzelm
# Date 1686857181 -7200
# Node ID 70041580b81e813d16e944849f76761c4dfbe997
# Parent  d47b2a04fc04640c5f5bf39bc9b3edeca75ebb29
tuned;

diff -r d47b2a04fc04 -r 70041580b81e src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Jun 15 21:24:37 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Jun 15 21:26:21 2023 +0200
@@ -126,7 +126,7 @@
         val shared_db = db.is_postgresql
         db.transaction_lock(Data.all_tables, create = true) {
           Data.clean_build(db)
-          if (shared_db) store.all_tables.create_lock(db)
+          if (shared_db) store.all_tables.lock(db, create = true)
         }
         db.vacuum(Data.all_tables ::: (if (shared_db) store.all_tables else SQL.Tables.empty))
       }
diff -r d47b2a04fc04 -r 70041580b81e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Jun 15 21:24:37 2023 +0200
+++ b/src/Pure/Tools/server.scala	Thu Jun 15 21:26:21 2023 +0200
@@ -398,8 +398,7 @@
     log: Logger = No_Logger
   ): (Info, Option[Server]) = {
     using(SQLite.open_database(Data.database, restrict = true)) { db =>
-      db.transaction {
-        Data.tables.create_lock(db)
+      db.transaction_lock(Data.tables, create = true) {
         list(db).filterNot(_.active).foreach(server_info =>
           db.execute_statement(Data.table.delete(sql = Data.name.where_equal(server_info.name))))
       }