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