author | wenzelm |
Sat, 02 Jan 2021 16:07:40 +0100 | |
changeset 73025 | 3e5a61d9f46a |
parent 73024 | 337e1b135d2f |
child 73026 | 237bd6318cc1 |
--- 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) }