src/Pure/Tools/sync.scala
changeset 76617 d5adc9126ae8
parent 76136 1bb677cceea4
child 77517 ede77a627b3a
--- a/src/Pure/Tools/sync.scala	Sun Dec 11 11:47:28 2022 +0100
+++ b/src/Pure/Tools/sync.scala	Sun Dec 11 12:52:46 2022 +0100
@@ -64,7 +64,7 @@
 
     for (hg <- afp_hg) {
       context.progress.echo_if(verbose, "\n* AFP repository:")
-      sync(hg, Rsync.append(target, "AFP"), afp_rev)
+      sync(hg, Url.append_path(target, "AFP"), afp_rev)
     }
 
     val images =
@@ -72,8 +72,9 @@
         dirs = afp_root.map(_ + Path.explode("thys")).toList)
     if (images.nonEmpty) {
       context.progress.echo_if(verbose, "\n* Session images:")
+      val heaps = Url.append_path(target, "heaps/")
       Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run,
-        args = List("--relative", "--") ::: images ::: List(Rsync.append(target, "heaps/"))).check
+        args = List("--relative", "--") ::: images ::: List(heaps)).check
     }
   }