src/Pure/Thy/store.scala
changeset 78400 63d55ba90a9f
parent 78396 7853d9072d1b
child 78510 8f45302a9ff0
--- a/src/Pure/Thy/store.scala	Tue Jul 18 21:06:11 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jul 18 23:03:39 2023 +0200
@@ -306,7 +306,8 @@
       port = options.int("build_database_port"),
       ssh_host = options.string("build_database_ssh_host"),
       ssh_port = options.int("build_database_ssh_port"),
-      ssh_user = options.string("build_database_ssh_user"))
+      ssh_user = options.string("build_database_ssh_user"),
+      synchronous_commit = options.string("build_database_synchronous_commit"))
 
   def maybe_open_database_server(server: SSH.Server = SSH.no_server): Option[SQL.Database] =
     if (build_database_server) Some(open_database_server(server = server)) else None