# HG changeset patch
# User wenzelm
# Date 1678816799 -3600
# Node ID 4240e9528586265908498a9e5739b58706da19b6
# Parent  a2a4adc268b8db8d69f0972778d6683c363a6cd0
tuned;

diff -r a2a4adc268b8 -r 4240e9528586 src/Pure/Tools/build_process.scala
--- 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,