| 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 } }