# HG changeset patch
# User wenzelm
# Date 1653996587 -7200
# Node ID 57e292106d713747ab2b9f243aa04b2fcc41914d
# Parent  c635368021b6bc0904431357077b8ea3951f9158
more operations;
tuned signature;

diff -r c635368021b6 -r 57e292106d71 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue May 31 13:14:46 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue May 31 13:29:47 2022 +0200
@@ -40,8 +40,8 @@
   val default_port = 22
   def make_port(port: Int): Int = if (port > 0) port else default_port
 
-  def port_suffix(port: Int, suffix: String = ":"): String =
-    if (port == default_port) "" else suffix + port
+  def port_suffix(port: Int): String =
+    if (port == default_port) "" else ":" + port
 
   def user_prefix(user: String): String =
     proper_string(user) match {
@@ -328,6 +328,9 @@
     override def hg_url: String =
       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
 
+    override def rsync_prefix: String =
+      user_prefix(nominal_user) + nominal_host + ":"
+
     override def toString: String =
       user_prefix(session.getUserName) + host + port_suffix(port) +
       (if (session.isConnected) "" else " (disconnected)")
@@ -489,6 +492,9 @@
 
     def hg_url: String = ""
 
+    def rsync_prefix: String = ""
+    def rsync_path(path: Path): String = rsync_prefix + expand_path(path)
+
     def expand_path(path: Path): Path = path.expand
     def bash_path(path: Path): String = File.bash_path(path)
     def is_dir(path: Path): Boolean = path.is_dir