# HG changeset patch
# User wenzelm
# Date 1663056884 -7200
# Node ID c5fd7947f585896c91b5237f8ace9a6394e5c3c3
# Parent  2bb6eb6df6c2b7490176655f86d930712124de53
tuned signature;

diff -r 2bb6eb6df6c2 -r c5fd7947f585 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Sep 13 10:11:53 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 10:14:44 2022 +0200
@@ -28,10 +28,6 @@
     }
   }
 
-  def port_suffix(port: Int): String = if (port > 0) ":" + port else ""
-
-  def user_prefix(user: String): String = if (user.nonEmpty) user + "@" else ""
-
 
   /* OpenSSH configuration and command-line */
 
@@ -106,9 +102,12 @@
   ) extends System {
     ssh =>
 
-    override def toString: String = user_prefix(user) + host + port_suffix(port)
+    def port_suffix: String = if (port > 0) ":" + port else ""
+    def user_prefix: String = if (user.nonEmpty) user + "@" else ""
+
+    override def toString: String = user_prefix + host + port_suffix
     override def hg_url: String = "ssh://" + toString + "/"
-    override def rsync_prefix: String = user_prefix(user) + host + ":"
+    override def rsync_prefix: String = user_prefix + host + ":"
 
 
     /* ssh commands */