# HG changeset patch
# User wenzelm
# Date 1688837306 -7200
# Node ID c0dc000d2a40c1984649b94ad671fd0be14bf4d0
# Parent  0bd366fad888476b6625e49c11217bd3efabce27
clarified operation: sequential vacuum to support obsolete versions 10 and 9.x;

diff -r 0bd366fad888 -r c0dc000d2a40 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sat Jul 08 19:14:09 2023 +0200
+++ b/src/Pure/General/sql.scala	Sat Jul 08 19:28:26 2023 +0200
@@ -609,9 +609,7 @@
     override def toString: String = name
 
     override def vacuum(tables: SQL.Tables = SQL.Tables.empty): Unit =
-      if (tables.list.nonEmpty) {
-        execute_statement("VACUUM" + if_proper(tables.list, " " + commas(tables.list.map(_.ident))))
-      }
+      for (table <- tables) execute_statement("VACUUM " + table.ident)
 
     override def now(): Date = {
       val now = SQL.Column.date("now")