# HG changeset patch
# User wenzelm
# Date 1654802895 -7200
# Node ID 460a25031ccd53d226aed5e8b084fb717f26d094
# Parent  18b77e4387f334e265a57a964f9846354fcd05bf
tuned;

diff -r 18b77e4387f3 -r 460a25031ccd src/Pure/General/ssh.scala
--- 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() })
         }