# HG changeset patch
# User wenzelm
# Date 1654535873 -7200
# Node ID 292d7a9dc8a369799c92b28113400f38c6019041
# Parent  b3fa6c79ed3ba3ae9589a4962dcbf76bc084c7d2
proper operation on String, not Path;

diff -r b3fa6c79ed3b -r 292d7a9dc8a3 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Jun 06 16:06:22 2022 +0200
+++ b/src/Pure/General/ssh.scala	Mon Jun 06 19:17:53 2022 +0200
@@ -493,7 +493,7 @@
     def hg_url: String = ""
 
     def rsync_prefix: String = ""
-    def rsync_path(path: Path): String = rsync_prefix + expand_path(path)
+    def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
 
     def expand_path(path: Path): Path = path.expand
     def bash_path(path: Path): String = File.bash_path(path)