# HG changeset patch # User wenzelm # Date 1654524382 -7200 # Node ID b3fa6c79ed3ba3ae9589a4962dcbf76bc084c7d2 # Parent 8c32f0210a1aa37ed5a5b4fbe05dcff5c7377bd4 clarified signature: cwd can be misleading --- changes meaning of target; diff -r 8c32f0210a1a -r b3fa6c79ed3b src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sun Jun 05 20:16:48 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon Jun 06 16:06:22 2022 +0200 @@ -421,7 +421,6 @@ } def rsync( - cwd: JFile = null, progress: Progress = new Progress, port: Int = SSH.default_port, verbose: Boolean = false, @@ -443,7 +442,7 @@ (if (list) " --list-only --no-human-readable" 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, echo = true) } def rsync_dir(target: String): String = {