# HG changeset patch
# User wenzelm
# Date 1689444499 -7200
# Node ID a9b544b6fc60a34c035a862a1ed5731716e272d9
# Parent  cd9c91ecbcb439cb52dbd8855bd7881cf4f877e3
potentially more robust: long-running operation only for build master, not workers;

diff -r cd9c91ecbcb4 -r a9b544b6fc60 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Jul 15 19:55:32 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sat Jul 15 20:08:19 2023 +0200
@@ -859,7 +859,7 @@
           Build_Process.Data.clean_build(db)
           store_tables.lock(db, create = true)
         }
-        db.vacuum(Build_Process.Data.tables ::: store_tables)
+        if (build_context.master) db.vacuum(Build_Process.Data.tables ::: store_tables)
         db
       }
     }