author | wenzelm |
Tue, 18 Jul 2023 12:55:43 +0200 | |
changeset 78393 | a2d22d519bf2 |
parent 78392 | 27c2fa1db6ed |
child 78394 | 761d12b043d0 |
--- a/src/Pure/Tools/build_process.scala Tue Jul 18 12:50:34 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Tue Jul 18 12:55:43 2023 +0200 @@ -870,8 +870,8 @@ if (store_tables) Store.Data.tables.lock(db, create = true) } if (build_context.master) { - db.vacuum(Build_Process.Data.tables.list ::: - (if (store_tables) Store.Data.tables.list else Nil)) + db.vacuum(Build_Process.Data.tables.list) + if (store_tables) db.vacuum(Store.Data.tables.list) } db }