# HG changeset patch
# User wenzelm
# Date 1689756979 -7200
# Node ID e25f1d343fa7f51d86a2f0242adca57f40a03683
# Parent  822ddccda899234d9c40032af5edb4cc76a37679
clarified options;

diff -r 822ddccda899 -r e25f1d343fa7 etc/options
--- a/etc/options	Wed Jul 19 10:42:40 2023 +0200
+++ b/etc/options	Wed Jul 19 10:56:19 2023 +0200
@@ -390,7 +390,7 @@
 option build_database_ssh_host : string = "" for connection
 option build_database_ssh_user : string = "" for connection
 option build_database_ssh_port : int = 0 for connection
-option build_database_synchronous_commit : string = "off" for connection
+option build_database_synchronous_commit : string = "off" (standard "on") for connection
   -- "see https://www.postgresql.org/docs/current/runtime-config-wal.html#GUC-SYNCHRONOUS-COMMIT"
 
 
@@ -406,7 +406,7 @@
 option build_log_ssh_port : int = 0 for connection
 option build_log_history : int = 30  -- "length of relevant history (in days)"
 option build_log_transaction_size : int = 1  -- "number of log files for each db update"
-option build_log_database_synchronous_commit : string = "off" for connection
+option build_log_database_synchronous_commit : string = "off" (standard "on") for connection
   -- "see https://www.postgresql.org/docs/current/runtime-config-wal.html#GUC-SYNCHRONOUS-COMMIT"
 
 
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