tuned;
authorwenzelm
Thu, 15 Jun 2023 21:26:21 +0200
changeset 78166 70041580b81e
parent 78165 d47b2a04fc04
child 78167 1b97502461a3
tuned;
src/Pure/Tools/build_process.scala
src/Pure/Tools/server.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))
       }
--- 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))))
       }