# HG changeset patch # User wenzelm # Date 1680973371 -7200 # Node ID 3e72fab0e699dce3dd52c1aaffc86b75c885725e # Parent ed68c546746cd19ff44d51657ced8215f1531f79 tuned output; diff -r ed68c546746c -r 3e72fab0e699 src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Sat Apr 08 18:59:58 2023 +0200 +++ b/src/Pure/General/rsync.scala Sat Apr 08 19:02:51 2023 +0200 @@ -26,6 +26,8 @@ archive: Boolean, protect_args: Boolean, ) { + override def toString: String = directory.toString + def no_progress: Context = new Context(directory, new Progress, archive, protect_args) def no_archive: Context = new Context(directory, progress, false, protect_args)