src/Pure/Admin/sync_repos.scala
changeset 75524 ff8012edac89
parent 75523 0dcaf0e5107b
child 75525 68162e4f60a7
--- a/src/Pure/Admin/sync_repos.scala	Tue Jun 07 12:32:53 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Tue Jun 07 16:47:57 2022 +0200
@@ -38,7 +38,7 @@
 
     for (hg <- afp_hg) {
       progress.echo_if(verbose, "\n* AFP repository:")
-      sync(hg, Rsync.rsync_dir(target) + "/AFP", afp_rev)
+      sync(hg, Rsync.append(target, "AFP"), afp_rev)
     }
   }