# 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 } }