# HG changeset patch # User wenzelm # Date 1654027848 -7200 # Node ID a5e0f1c66c265a512f109b25b1f8398d8132f4cb # Parent ee51db628e711c438df6b86796730ef137a99fc8 clarified signature (again); diff -r ee51db628e71 -r a5e0f1c66c26 src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala Tue May 31 16:01:30 2022 +0200 +++ b/src/Pure/Admin/sync_repos.scala Tue May 31 22:10:48 2022 +0200 @@ -39,7 +39,8 @@ val id_path = tmp_dir + Path.explode("ISABELLE_ID") File.write(id_path, hg.id(rev = rev)) Isabelle_System.rsync(port = port, thorough = thorough, - args = List(File.standard_path(id_path), target_dir + "etc/")) + args = List(File.standard_path(id_path), target_dir + "etc/") + ).check } } diff -r ee51db628e71 -r a5e0f1c66c26 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue May 31 16:01:30 2022 +0200 +++ b/src/Pure/General/mercurial.scala Tue May 31 22:10:48 2022 +0200 @@ -284,7 +284,8 @@ Isabelle_System.rsync( progress = progress, port = port, verbose = verbose, thorough = thorough, dry_run = dry_run, clean = clean, filter = filter, - args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)) + args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target) + ).check } } diff -r ee51db628e71 -r a5e0f1c66c26 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Tue May 31 16:01:30 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Tue May 31 22:10:48 2022 +0200 @@ -430,7 +430,7 @@ clean: Boolean = false, filter: List[String] = Nil, args: List[String] = Nil - ): Unit = { + ): Process_Result = { val script = "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) + (if (verbose || dry_run) " --verbose" else "") + @@ -439,7 +439,7 @@ (if (clean) " --delete-excluded" else "") + filter.map(s => " --filter=" + Bash.string(s)).mkString + (if (args.nonEmpty) " " + Bash.strings(args) else "") - progress.bash(script, cwd = cwd, echo = true).check + progress.bash(script, cwd = cwd, echo = true) } def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {