diff -r 822ddccda899 -r e25f1d343fa7 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Wed Jul 19 10:42:40 2023 +0200 +++ b/src/Pure/General/sql.scala Wed Jul 19 10:56:19 2023 +0200 @@ -653,7 +653,9 @@ val db = new Database(connection, print, server, server_close) try { - db.execute_statement("SET synchronous_commit = " + SQL.string(synchronous_commit)) + if (synchronous_commit.nonEmpty) { + db.execute_statement("SET synchronous_commit = " + SQL.string(synchronous_commit)) + } } catch { case exn: Throwable => db.close(); throw exn } @@ -689,7 +691,7 @@ ssh_host: String = "", ssh_port: Int = 0, ssh_user: String = "", - synchronous_commit: String = "off" + synchronous_commit: String = "" ): PostgreSQL.Database = { val db_server = if (server.defined) server