--- a/src/Pure/Tools/build_process.scala Tue Mar 14 18:57:34 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Tue Mar 14 18:59:59 2023 +0100
@@ -368,12 +368,8 @@
Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.defined)),
List.from[String], res => res.string(Base.build_uuid))
- val tables =
- all_tables.filter(table =>
- table.columns.exists(column => column.name == Generic.build_uuid.name))
-
if (old.nonEmpty) {
- for (table <- tables) {
+ for (table <- build_uuid_tables) {
db.execute_statement(table.delete(sql = Generic.build_uuid.where_member(old)))
}
}
@@ -826,6 +822,10 @@
Results.table,
Host.Data.Node_Info.table)
+ val build_uuid_tables =
+ all_tables.filter(table =>
+ table.columns.exists(column => column.name == Generic.build_uuid.name))
+
def pull_database(
db: SQL.Database,
worker_uuid: String,