--- a/src/Pure/General/ssh.scala Wed Mar 18 22:22:16 2020 +0100
+++ b/src/Pure/General/ssh.scala Thu Mar 19 11:27:54 2020 +0100
@@ -83,10 +83,12 @@
new Context(options, jsch)
}
- def open_session(options: Options, host: String, user: String = "", port: Int = 0,
+ def open_session(options: Options,
+ host: String, user: String = "", port: Int = 0, actual_host: String = "",
proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
permissive: Boolean = false): Session =
- init_context(options).open_session(host = host, user = user, port = port,
+ init_context(options).open_session(
+ host = host, user = user, port = port, actual_host = actual_host,
proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
permissive = permissive)
@@ -120,16 +122,18 @@
proper_string(nominal_user) getOrElse user)
}
- def open_session(host: String, user: String = "", port: Int = 0,
+ def open_session(
+ host: String, user: String = "", port: Int = 0, actual_host: String = "",
proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
permissive: Boolean = false): Session =
{
- if (proxy_host == "") connect_session(host = host, user = user, port = port)
+ val connect_host = proper_string(actual_host) getOrElse host
+ if (proxy_host == "") connect_session(host = connect_host, user = user, port = port)
else {
val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
val fw =
- try { proxy.port_forwarding(remote_host = host, remote_port = make_port(port)) }
+ try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
catch { case exn: Throwable => proxy.close; throw exn }
try {