# HG changeset patch
# User wenzelm
# Date 1653837998 -7200
# Node ID 1f0016095195fcba99d4c4c7c857182194992606
# Parent  1148c190eb9ba573a1cc3f2590b3ea68c32ab592
tuned;

diff -r 1148c190eb9b -r 1f0016095195 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun May 29 16:25:37 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 29 17:26:38 2022 +0200
@@ -256,16 +256,18 @@
       verbose: Boolean = false,
       dry_run: Boolean = false,
       clean: Boolean = false,
-      filter: List[String] = Nil
+      filter: List[String] = Nil,
     ): Unit = {
-      Isabelle_System.with_tmp_file("exclude") { exclude_path =>
+      Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
+        val exclude_path = tmp_dir + Path.explode("exclude")
         val exclude = status(options = "--unknown --ignored --no-status")
         File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
+
+        val options = List("--exclude-from=" + exclude_path.implode)
+        val source = ssh.rsync_url + root.expand.implode + "/."
         Isabelle_System.rsync(
           progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter,
-          args = List("--prune-empty-dirs", "--exclude-from=" + exclude_path.implode,
-            "--", ssh.rsync_url + root.expand.implode + "/.", target)
-        ).check
+          args = List("--prune-empty-dirs") ::: options ::: List("--", source, target)).check
       }
     }