# HG changeset patch # User wenzelm # Date 1688562106 -7200 # Node ID 3e11f510b3f679ea1266c1d5ffc54da4227a85b1 # Parent 400aecdfd71f3cd6a781ee648f1a0df06eee3c8c# Parent 50a949d316d357fc7902f2b795d2f13a54cd91f2 merged diff -r 400aecdfd71f -r 3e11f510b3f6 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Tue Jul 04 12:53:01 2023 +0100 +++ b/src/Pure/General/sql.scala Wed Jul 05 15:01:46 2023 +0200 @@ -642,7 +642,7 @@ // see https://www.postgresql.org/docs/current/explicit-locking.html override def lock_tables(tables: List[SQL.Table]): PostgreSQL.Source = - "LOCK TABLE " + tables.mkString(", ") + " IN ACCESS EXCLUSIVE MODE" + if_proper(tables, "LOCK TABLE " + tables.mkString(", ") + " IN ACCESS EXCLUSIVE MODE") /* notifications: IPC via database server */ diff -r 400aecdfd71f -r 3e11f510b3f6 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Tue Jul 04 12:53:01 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Wed Jul 05 15:01:46 2023 +0200 @@ -421,7 +421,7 @@ def read_sessions_domain(db: SQL.Database, build_uuid: String = ""): Set[String] = db.execute_query_statement( Sessions.table.select(List(Sessions.name), - sql = if_proper(build_uuid, Sessions.name.where_equal(build_uuid))), + sql = if_proper(build_uuid, Sessions.build_uuid.where_equal(build_uuid))), Set.from[String], res => res.string(Sessions.name)) def read_sessions(db: SQL.Database, @@ -845,13 +845,12 @@ private val _build_database: Option[SQL.Database] = try { for (db <- store.maybe_open_build_database()) yield { - val shared_db = db.is_postgresql + val more_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty Build_Process.Data.transaction_lock(db, create = true) { Build_Process.Data.clean_build(db) - if (shared_db) Store.Data.tables.lock(db, create = true) + more_tables.lock(db, create = true) } - Build_Process.Data.vacuum(db, - more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty) + Build_Process.Data.vacuum(db, more_tables = more_tables) db } } @@ -1081,7 +1080,7 @@ start_worker() if (build_context.master && !build_context.worker_active) { - progress.echo("Waiting for external workers ...") + build_progress.echo("Waiting for external workers ...") } try {