# HG changeset patch # User wenzelm # Date 1653822390 -7200 # Node ID d7035cfa1f14a74ff431e8c9a1c9b904024a122c # Parent ff6d4b48f23b20f747138cea1345e201249ad355 clarified signature; diff -r ff6d4b48f23b -r d7035cfa1f14 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sun May 29 11:45:32 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Sun May 29 13:06:30 2022 +0200 @@ -430,7 +430,7 @@ ): Process_Result = { val script = "rsync --protect-args --archive" + - (if (verbose) " --verbose" else "") + + (if (verbose || dry_run) " --verbose" else "") + (if (dry_run) " --dry-run" else "") + (if (clean) " --delete-excluded" else "") + (if (args.nonEmpty) " " + Bash.strings(args) else "")