--- 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
}
}
--- 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
}
}
--- 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 = {