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