# HG changeset patch
# User wenzelm
# Date 1653860998 -7200
# Node ID d8ee3e4d74ef5f7d2e8e25c0ba4015f49c6832d8
# Parent  f37df3759770af38f1aad8f3a655fcfd07b1e0ca
clarified signature;

diff -r f37df3759770 -r d8ee3e4d74ef src/Pure/Admin/sync_repos.scala
--- 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/"))
       }
     }
 
diff -r f37df3759770 -r d8ee3e4d74ef src/Pure/General/mercurial.scala
--- 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))
       }
     }
 
diff -r f37df3759770 -r d8ee3e4d74ef src/Pure/System/isabelle_system.scala
--- 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 = {