# HG changeset patch
# User wenzelm
# Date 1689339408 -7200
# Node ID 1932737e55a99cb1dc20e3cb28573c1ac2c4777a
# Parent  ef1664be143d0744b2ad7d2edb88713b907a0d12
clarified signature: follow Store.open_database;

diff -r ef1664be143d -r 1932737e55a9 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Jul 14 14:25:53 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Jul 14 14:56:48 2023 +0200
@@ -816,7 +816,7 @@
   def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
     new Store(options, cache)
 
-  class Store private[Build_Log](options: Options, val cache: XML.Cache) {
+  class Store private[Build_Log](val options: Options, val cache: XML.Cache) {
     override def toString: String = {
       val s =
         Exn.capture { open_database() } match {
@@ -835,16 +835,17 @@
       database: String = options.string("build_log_database_name"),
       host: String = options.string("build_log_database_host"),
       port: Int = options.int("build_log_database_port"),
-      ssh_host: String = options.string("build_log_ssh_host"),
-      ssh_user: String = options.string("build_log_ssh_user"),
-      ssh_port: Int = options.int("build_log_ssh_port")
+      ssh: Option[SSH.Session] =
+        proper_string(options.string("build_log_ssh_host")).map(ssh_host =>
+          SSH.open_session(options,
+            host = ssh_host,
+            user = options.string("build_log_ssh_user"),
+            port = options.int("build_log_ssh_port"))),
+      ssh_close: Boolean = true
     ): PostgreSQL.Database = {
       PostgreSQL.open_database(
         user = user, password = password, database = database, host = host, port = port,
-        ssh =
-          if (ssh_host == "") None
-          else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = ssh_port)),
-        ssh_close = true)
+        ssh = ssh, ssh_close = ssh_close)
     }
 
     def snapshot_database(