# HG changeset patch # User wenzelm # Date 1654614651 -7200 # Node ID 57b6a28e4ebada9174b20a8ddc145aa1c89f7e26 # Parent 68162e4f60a790db38e58544644da616cdb2da46 tuned signature; diff -r 68162e4f60a7 -r 57b6a28e4eba src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue Jun 07 17:07:10 2022 +0200 +++ b/src/Pure/General/mercurial.scala Tue Jun 07 17:10:51 2022 +0200 @@ -304,10 +304,10 @@ require(ssh == SSH.Local, "local repository required") Isabelle_System.with_tmp_dir("sync") { tmp_dir => - Rsync.rsync_init(context, target) + Rsync.init(context, target) val list = - Rsync.rsync(context, list = true, + Rsync.exec(context, list = true, args = List("--", Rsync.terminate(target)) ).check.out_lines.filterNot(_.endsWith(" .")) if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { @@ -320,7 +320,7 @@ val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" - Rsync.rsync_init(context, target, + Rsync.init(context, target, contents = File.Content(Hg_Sync.PATH_ID, id_content) :: File.Content(Hg_Sync.PATH_LOG, log_content) :: @@ -346,7 +346,7 @@ val protect = (Hg_Sync.PATH :: contents.map(_.path)) .map(path => "protect /" + File.standard_path(path)) - Rsync.rsync(context, + Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run, diff -r 68162e4f60a7 -r 57b6a28e4eba src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Tue Jun 07 17:07:10 2022 +0200 +++ b/src/Pure/General/rsync.scala Tue Jun 07 17:10:51 2022 +0200 @@ -13,7 +13,7 @@ "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) } - def rsync( + def exec( context: Context, verbose: Boolean = false, thorough: Boolean = false, @@ -37,13 +37,13 @@ context.progress.bash(script, echo = true) } - def rsync_init(context: Context, target: String, + def init(context: Context, target: String, contents: List[File.Content] = Nil ): Unit = Isabelle_System.with_tmp_dir("sync") { tmp_dir => val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init")) contents.foreach(_.write(init_dir)) - rsync(context, thorough = true, + exec(context, thorough = true, args = List(File.bash_path(init_dir) + "/.", target)).check }