# HG changeset patch
# User wenzelm
# Date 1654724994 -7200
# Node ID 179a3b028b0ac75bfeb48813907993c297d7e75d
# Parent  1910054f8c391056f58b4deba7a1e486a51d50e1
proper nominal_port, notably for port forwarding;

diff -r 1910054f8c39 -r 179a3b028b0a src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Wed Jun 08 15:36:27 2022 +0100
+++ b/src/Pure/Admin/build_history.scala	Wed Jun 08 23:49:54 2022 +0200
@@ -535,7 +535,7 @@
     def sync_repos(target: Path, accurate: Boolean = false,
       rev: String = "", afp_rev: String = "", afp: Boolean = false
     ): Unit = {
-      val context = Rsync.Context(progress, port = ssh.port, protect_args = protect_args)
+      val context = Rsync.Context(progress, port = ssh.nominal_port, protect_args = protect_args)
       Sync_Repos.sync_repos(context, ssh.rsync_path(target),
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
diff -r 1910054f8c39 -r 179a3b028b0a src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Jun 08 15:36:27 2022 +0100
+++ b/src/Pure/General/ssh.scala	Wed Jun 08 23:49:54 2022 +0200
@@ -107,6 +107,7 @@
       host_key_permissive: Boolean = false,
       nominal_host: String = "",
       nominal_user: String = "",
+      nominal_port: Int = 0,
       on_close: () => Unit = () => ()
     ): Session = {
       val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
@@ -126,7 +127,8 @@
       session.connect(connect_timeout(options))
       new Session(options, session, on_close,
         proper_string(nominal_host) getOrElse host,
-        proper_string(nominal_user) getOrElse user)
+        proper_string(nominal_user) getOrElse user,
+        if (nominal_port > 0) nominal_port else port)
     }
 
     def open_session(
@@ -151,7 +153,7 @@
         try {
           connect_session(host = fw.local_host, port = fw.local_port,
             host_key_permissive = permissive,
-            nominal_host = host, nominal_user = user, user = user,
+            nominal_host = host, nominal_port = port, nominal_user = user, user = user,
             on_close = { () => fw.close(); proxy.close() })
         }
         catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
@@ -317,13 +319,13 @@
     val session: JSch_Session,
     on_close: () => Unit,
     val nominal_host: String,
-    val nominal_user: String
+    val nominal_user: String,
+    val nominal_port: Int
   ) extends System {
     def update_options(new_options: Options): Session =
-      new Session(new_options, session, on_close, nominal_host, nominal_user)
+      new Session(new_options, session, on_close, nominal_host, nominal_user, nominal_port)
 
     def host: String = if (session.getHost == null) "" else session.getHost
-    def port: Int = session.getPort
 
     override def hg_url: String =
       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
@@ -332,7 +334,7 @@
       user_prefix(nominal_user) + nominal_host + ":"
 
     override def toString: String =
-      user_prefix(session.getUserName) + host + port_suffix(port) +
+      user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
       (if (session.isConnected) "" else " (disconnected)")