proper ssh_port (amending ffd8283b7be0);
authorwenzelm
Sat, 02 Jan 2021 16:07:40 +0100
changeset 73025 3e5a61d9f46a
parent 73024 337e1b135d2f
child 73026 237bd6318cc1
proper ssh_port (amending ffd8283b7be0);
src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Jan 02 15:58:48 2021 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Jan 02 16:07:40 2021 +0100
@@ -874,7 +874,7 @@
         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 = port)),
+          else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = ssh_port)),
         ssh_close = true)
     }