# HG changeset patch
# User wenzelm
# Date 1678978549 -3600
# Node ID e7d8e990d37856b3e111e933e1b5116bbc20a84e
# Parent  daaaf59375e93cb5fdadf29291a01800386c0624
proper vacuum of session_info tables: only once per build process;

diff -r daaaf59375e9 -r e7d8e990d378 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Mar 16 15:46:10 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 16 15:55:49 2023 +0100
@@ -123,11 +123,13 @@
 
     def prepare_database(): Unit = {
       using_option(store.open_build_database()) { db =>
+        val shared_db = db.is_postgresql
         db.transaction {
           Data.all_tables.create_lock(db)
           Data.clean_build(db)
+          if (shared_db) store.all_tables.create_lock(db)
         }
-        db.vacuum(Data.all_tables)
+        db.vacuum(Data.all_tables ::: (if (shared_db) store.all_tables else SQL.Tables.empty))
       }
     }