# HG changeset patch
# User wenzelm
# Date 1653737594 -7200
# Node ID a1c7829ac2def459dbfaf0a194e601f25ba99f2b
# Parent  5f2a1efd05602097bca68d46cdd0f694a956a744
support rsync;

diff -r 5f2a1efd0560 -r a1c7829ac2de src/Pure/Admin/build_cygwin.scala
--- 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,
diff -r 5f2a1efd0560 -r a1c7829ac2de src/Pure/System/isabelle_system.scala
--- 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(