# HG changeset patch # User wenzelm # Date 1678815812 -3600 # Node ID fd553b54fce155b234f35e51ef4913e8b341c407 # Parent 136ab737a36d52d809553f0470d2d7bcdf414685 more thorough cleanup; diff -r 136ab737a36d -r fd553b54fce1 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))) } }