--- a/src/Pure/Admin/sync_repos.scala Sun May 29 23:47:53 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala Sun May 29 23:49:58 2022 +0200
@@ -33,7 +33,7 @@
Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir =>
val id_path = tmp_dir + Path.explode("ISABELLE_ID")
File.write(id_path, isabelle_hg.id(rev = rev))
- Isabelle_System.rsync(args = List(File.standard_path(id_path), target_dir + "etc/")).check
+ Isabelle_System.rsync(args = List(File.standard_path(id_path), target_dir + "etc/"))
}
}
--- a/src/Pure/General/mercurial.scala Sun May 29 23:47:53 2022 +0200
+++ b/src/Pure/General/mercurial.scala Sun May 29 23:49:58 2022 +0200
@@ -279,7 +279,7 @@
}
Isabelle_System.rsync(
progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter,
- args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)).check
+ args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target))
}
}
--- a/src/Pure/System/isabelle_system.scala Sun May 29 23:47:53 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Sun May 29 23:49:58 2022 +0200
@@ -428,7 +428,7 @@
clean: Boolean = false,
filter: List[String] = Nil,
args: List[String] = Nil
- ): Process_Result = {
+ ): Unit = {
val script =
"rsync --protect-args --archive" +
(if (verbose || dry_run) " --verbose" else "") +
@@ -436,7 +436,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)
+ progress.bash(script, cwd = cwd, echo = true).check
}
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {