--- a/src/Pure/Admin/build_cygwin.scala Fri May 27 16:16:45 2022 +0200
+++ b/src/Pure/Admin/build_cygwin.scala Sat May 28 13:33:14 2022 +0200
@@ -11,7 +11,7 @@
val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021-1"
val packages: List[String] =
- List("curl", "libgmp-devel", "nano", "unzip")
+ List("curl", "libgmp-devel", "nano", "rsync", "unzip")
def build_cygwin(progress: Progress,
mirror: String = default_mirror,
--- a/src/Pure/System/isabelle_system.scala Fri May 27 16:16:45 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Sat May 28 13:33:14 2022 +0200
@@ -420,6 +420,24 @@
else error("Expected to find GNU tar executable")
}
+ def rsync(
+ cwd: JFile = null,
+ progress: Progress = new Progress,
+ echo: Boolean = false,
+ verbose: Boolean = false,
+ dry_run: Boolean = false,
+ purge: Boolean = false,
+ args: List[String] = Nil
+ ): Process_Result = {
+ val script =
+ "rsync --protect-args --archive" +
+ (if (verbose) " --verbose" else "") +
+ (if (dry_run) " --dry-run" else "") +
+ (if (purge) " --delete-excluded" else "") +
+ (if (args.nonEmpty) " " + Bash.strings(args) else "")
+ progress.bash(script, cwd = cwd, echo = echo || verbose)
+ }
+
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
with_tmp_file("patch") { patch =>
Isabelle_System.bash(