clarified options;
authorwenzelm
Wed, 19 Jul 2023 10:56:19 +0200
changeset 78402 e25f1d343fa7
parent 78401 822ddccda899
child 78403 a09929ad05b6
clarified options;
etc/options
src/Pure/General/sql.scala
--- 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"
 
 
--- 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