proper vacuum of session_info tables: only once per build process;
authorwenzelm
Thu, 16 Mar 2023 15:55:49 +0100
changeset 77678 e7d8e990d378
parent 77677 daaaf59375e9
child 77679 e92000492895
proper vacuum of session_info tables: only once per build process;
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))
       }
     }