# HG changeset patch
# User wenzelm
# Date 1692608130 -7200
# Node ID 5f4ca329fde42fd4e0334faed4819e8b66d4ddeb
# Parent  3be0437759cf63900daa897ae5f934305d9aab61
minor performance tuning: avoid multiple db roundtrips;

diff -r 3be0437759cf -r 5f4ca329fde4 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Aug 21 10:53:50 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Mon Aug 21 10:55:30 2023 +0200
@@ -380,9 +380,8 @@
           List.from[String], res => res.string(Base.build_uuid))
 
       if (old.nonEmpty) {
-        for (table <- build_uuid_tables) {
-          db.execute_statement(table.delete(sql = Generic.build_uuid.where_member(old)))
-        }
+        val sql = Generic.build_uuid.where_member(old)
+        db.execute_statement(SQL.MULTI(build_uuid_tables.map(_.delete(sql = sql))))
       }
     }