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) } }