# HG changeset patch
# User wenzelm
# Date 1688732273 -7200
# Node ID 8c999990262ce20b0355efd4e6546418af13fe3c
# Parent  968b5b981a8cf18711719d3e0dbc7d241b862815
clarified signature;

diff -r 968b5b981a8c -r 8c999990262c src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Jul 07 14:10:36 2023 +0200
+++ b/src/Pure/General/sql.scala	Fri Jul 07 14:17:53 2023 +0200
@@ -260,9 +260,6 @@
       if (synchronized) db.synchronized { run } else run
     }
 
-    def vacuum(db: Database, more_tables: Tables = Tables.empty): Unit =
-      db.vacuum(tables = tables ::: more_tables)
-
     def make_table(name: String, columns: List[Column], body: String = ""): Table = {
       val table_name =
         List(proper_string(table_prefix), proper_string(name)).flatten.mkString("_")
diff -r 968b5b981a8c -r 8c999990262c src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Fri Jul 07 14:10:36 2023 +0200
+++ b/src/Pure/System/progress.scala	Fri Jul 07 14:17:53 2023 +0200
@@ -289,7 +289,7 @@
         stmt.long(10) = 0L
       })
     }
-    if (context_uuid == _agent_uuid) Progress.Data.vacuum(db)
+    if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.tables)
   }
 
   def exit(close: Boolean = false): Unit = synchronized {
diff -r 968b5b981a8c -r 8c999990262c src/Pure/Tools/build_process.scala
--- 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
       }
     }