# HG changeset patch
# User wenzelm
# Date 1654027848 -7200
# Node ID a5e0f1c66c265a512f109b25b1f8398d8132f4cb
# Parent  ee51db628e711c438df6b86796730ef137a99fc8
clarified signature (again);

diff -r ee51db628e71 -r a5e0f1c66c26 src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala	Tue May 31 16:01:30 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Tue May 31 22:10:48 2022 +0200
@@ -39,7 +39,8 @@
         val id_path = tmp_dir + Path.explode("ISABELLE_ID")
         File.write(id_path, hg.id(rev = rev))
         Isabelle_System.rsync(port = port, thorough = thorough,
-          args = List(File.standard_path(id_path), target_dir + "etc/"))
+          args = List(File.standard_path(id_path), target_dir + "etc/")
+        ).check
       }
     }
 
diff -r ee51db628e71 -r a5e0f1c66c26 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue May 31 16:01:30 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue May 31 22:10:48 2022 +0200
@@ -284,7 +284,8 @@
         Isabelle_System.rsync(
           progress = progress, port = port, verbose = verbose, thorough = thorough,
           dry_run = dry_run, clean = clean, filter = filter,
-          args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target))
+          args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)
+        ).check
       }
     }
 
diff -r ee51db628e71 -r a5e0f1c66c26 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue May 31 16:01:30 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue May 31 22:10:48 2022 +0200
@@ -430,7 +430,7 @@
     clean: Boolean = false,
     filter: List[String] = Nil,
     args: List[String] = Nil
-  ): Unit = {
+  ): Process_Result = {
     val script =
       "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
         (if (verbose || dry_run) " --verbose" else "") +
@@ -439,7 +439,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).check
+    progress.bash(script, cwd = cwd, echo = true)
   }
 
   def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {