support rsync;
authorwenzelm
Sat, 28 May 2022 13:33:14 +0200
changeset 75468 a1c7829ac2de
parent 75466 5f2a1efd0560
child 75469 c2fb64822a7b
support rsync;
src/Pure/Admin/build_cygwin.scala
src/Pure/System/isabelle_system.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,
--- 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(