more thorough cleanup;
authorwenzelm
Tue, 14 Mar 2023 18:43:32 +0100
changeset 77656 fd553b54fce1
parent 77655 136ab737a36d
child 77657 a2a4adc268b8
more thorough cleanup;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 18:29:07 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 18:43:32 2023 +0100
@@ -372,8 +372,12 @@
           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 <- List(Base.table, Sessions.table, Progress.table, Workers.table)) {
+        for (table <- tables) {
           db.execute_statement(table.delete(sql = Generic.build_uuid.where_member(old)))
         }
       }