--- a/src/Pure/General/ssh.scala Thu Jun 09 00:10:18 2022 +0200
+++ b/src/Pure/General/ssh.scala Thu Jun 09 21:28:15 2022 +0200
@@ -104,19 +104,20 @@
host: String,
user: String = "",
port: Int = 0,
- host_key_permissive: Boolean = false,
+ permissive: Boolean = false,
nominal_host: String = "",
nominal_user: String = "",
nominal_port: Option[Int] = None,
on_close: () => Unit = () => ()
): Session = {
- val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
+ val connect_port = make_port(port)
+ val session = jsch.getSession(proper_string(user).orNull, host, connect_port)
session.setUserInfo(No_User_Info)
session.setServerAliveInterval(alive_interval(options))
session.setServerAliveCountMax(alive_count_max(options))
session.setConfig("MaxAuthTries", "3")
- if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no")
+ if (permissive) session.setConfig("StrictHostKeyChecking", "no")
if (nominal_host != "") session.setHostKeyAlias(nominal_host)
if (options.bool("ssh_compression")) {
@@ -128,7 +129,7 @@
new Session(options, session, on_close,
proper_string(nominal_host) getOrElse host,
proper_string(nominal_user) getOrElse user,
- nominal_port.getOrElse(make_port(port)))
+ nominal_port getOrElse connect_port)
}
def open_session(
@@ -142,19 +143,22 @@
permissive: Boolean = false
): Session = {
val connect_host = proper_string(actual_host) getOrElse host
- if (proxy_host == "") connect_session(host = connect_host, user = user, port = port)
+ val connect_port = make_port(port)
+ if (proxy_host == "") connect_session(host = connect_host, user = user, port = connect_port)
else {
val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
val fw =
- try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
+ try { proxy.port_forwarding(remote_host = connect_host, remote_port = connect_port) }
catch { case exn: Throwable => proxy.close(); throw exn }
try {
- connect_session(host = fw.local_host, port = fw.local_port,
- host_key_permissive = permissive,
+ connect_session(
+ host = fw.local_host,
+ port = fw.local_port,
+ permissive = permissive,
nominal_host = host,
- nominal_port = Some(make_port(port)),
+ nominal_port = Some(connect_port),
nominal_user = user, user = user,
on_close = { () => fw.close(); proxy.close() })
}