# HG changeset patch
# User wenzelm
# Date 1654726218 -7200
# Node ID 18b77e4387f334e265a57a964f9846354fcd05bf
# Parent  218dd201e24d343906fcd7f23b278eea85a2832d
proper make_port for regular situation;
tuned whitespace;

diff -r 218dd201e24d -r 18b77e4387f3 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Jun 09 00:01:34 2022 +0200
+++ b/src/Pure/General/ssh.scala	Thu Jun 09 00:10:18 2022 +0200
@@ -128,7 +128,7 @@
       new Session(options, session, on_close,
         proper_string(nominal_host) getOrElse host,
         proper_string(nominal_user) getOrElse user,
-        nominal_port.getOrElse(port))
+        nominal_port.getOrElse(make_port(port)))
     }
 
     def open_session(
@@ -154,8 +154,8 @@
           connect_session(host = fw.local_host, port = fw.local_port,
             host_key_permissive = permissive,
             nominal_host = host,
-	    nominal_port = Some(make_port(port)),
-	    nominal_user = user, user = user,
+            nominal_port = Some(make_port(port)),
+            nominal_user = user, user = user,
             on_close = { () => fw.close(); proxy.close() })
         }
         catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }