src/Pure/Admin/build_log.scala
changeset 78400 63d55ba90a9f
parent 78389 41e8ae87184d
child 78592 fdfe9b91d96e
--- a/src/Pure/Admin/build_log.scala	Tue Jul 18 21:06:11 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Jul 18 23:03:39 2023 +0200
@@ -841,7 +841,8 @@
         port = options.int("build_log_database_port"),
         ssh_host = options.string("build_log_ssh_host"),
         ssh_port = options.int("build_log_ssh_port"),
-        ssh_user = options.string("build_log_ssh_user"))
+        ssh_user = options.string("build_log_ssh_user"),
+        synchronous_commit = options.string("build_log_database_synchronous_commit"))
 
     def snapshot_database(
       db: PostgreSQL.Database,