src/Pure/General/sql.scala
changeset 78402 e25f1d343fa7
parent 78400 63d55ba90a9f
child 78422 dcaf6f33d94d
--- 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