# HG changeset patch
# User wenzelm
# Date 1689677743 -7200
# Node ID a2d22d519bf27a80b6a385a5c96b6bb53115f307
# Parent  27c2fa1db6edc0fe2500929463aee4650d498a9f
more robust: implicit locking of tables in standard order;

diff -r 27c2fa1db6ed -r a2d22d519bf2 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Jul 18 12:50:34 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Tue Jul 18 12:55:43 2023 +0200
@@ -870,8 +870,8 @@
           if (store_tables) Store.Data.tables.lock(db, create = true)
         }
         if (build_context.master) {
-          db.vacuum(Build_Process.Data.tables.list :::
-            (if (store_tables) Store.Data.tables.list else Nil))
+          db.vacuum(Build_Process.Data.tables.list)
+          if (store_tables) db.vacuum(Store.Data.tables.list)
         }
         db
       }