# HG changeset patch # User wenzelm # Date 1670759566 -3600 # Node ID d5adc9126ae8d61ffeef61fe631f088a8d3383a7 # Parent e6c11ef4fb51962e46216ab20d7e46cf86dd66d0 clarified signature; diff -r e6c11ef4fb51 -r d5adc9126ae8 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sun Dec 11 11:47:28 2022 +0100 +++ b/src/Pure/General/mercurial.scala Sun Dec 11 12:52:46 2022 +0100 @@ -309,7 +309,7 @@ Rsync.init(context0, target) val list = - Rsync.exec(context0, list = true, args = List("--", Rsync.direct(target))) + Rsync.exec(context0, list = true, args = List("--", Url.direct_path(target))) .check.out_lines.filterNot(_.endsWith(" .")) if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { error("No .hg_sync meta data in " + quote(target)) @@ -355,7 +355,7 @@ prune_empty_dirs = true, filter = protect ::: filter, args = List("--exclude-from=" + exclude_path.implode, "--", - Rsync.direct(source), target) + Url.direct_path(source), target) ).check } } diff -r e6c11ef4fb51 -r d5adc9126ae8 src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Sun Dec 11 11:47:28 2022 +0100 +++ b/src/Pure/General/rsync.scala Sun Dec 11 12:52:46 2022 +0100 @@ -58,13 +58,4 @@ List(if (contents.nonEmpty) "--archive" else "--dirs", File.bash_path(init_dir) + "/.", target)).check } - - def direct(prefix: String): String = - if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "." - else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix - else prefix + "/." - - def append(prefix: String, suffix: String): String = - if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix - else prefix + "/" + suffix } diff -r e6c11ef4fb51 -r d5adc9126ae8 src/Pure/General/url.scala --- a/src/Pure/General/url.scala Sun Dec 11 11:47:28 2022 +0100 +++ b/src/Pure/General/url.scala Sun Dec 11 12:52:46 2022 +0100 @@ -100,4 +100,16 @@ def canonical_file(uri: String): JFile = File.canonical(parse_file(uri)) def canonical_file_name(uri: String): String = canonical_file(uri).getPath + + + /* generic path notation: local, ssh, rsync, http */ + + def direct_path(prefix: String): String = + if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "." + else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix + else prefix + "/." + + def append_path(prefix: String, suffix: String): String = + if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix + else prefix + "/" + suffix } diff -r e6c11ef4fb51 -r d5adc9126ae8 src/Pure/Tools/sync.scala --- 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 } }