src/Pure/Tools/build_process.scala
changeset 78263 8c999990262c
parent 78254 50a949d316d3
child 78264 c8fde312c895
--- a/src/Pure/Tools/build_process.scala	Fri Jul 07 14:10:36 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jul 07 14:17:53 2023 +0200
@@ -850,7 +850,7 @@
           Build_Process.Data.clean_build(db)
           more_tables.lock(db, create = true)
         }
-        Build_Process.Data.vacuum(db, more_tables = more_tables)
+        db.vacuum(Build_Process.Data.tables ::: more_tables)
         db
       }
     }