# HG changeset patch
# User wenzelm
# Date 1355522675 -3600
# Node ID f4aac67a6405a5553f831f5db78d50246582f58f
# Parent  3b68e5760a2d840a422192bbfd767a21ab79821c
tuned;

diff -r 3b68e5760a2d -r f4aac67a6405 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Dec 14 21:50:21 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Dec 14 23:04:35 2012 +0100
@@ -39,6 +39,8 @@
       if (this eq other) this
       else if (rep.isEmpty) other
       else (this /: other.entries)(_ + _)
+
+    override def toString: String = entries.mkString("Results(", ", ", ")")
   }