# HG changeset patch
# User wenzelm
# Date 1489516839 -3600
# Node ID fe6d2cd61009d70ac5e0babcfcf5568a82ad8187
# Parent  1d6e9048cb6256d70407711d81c9389baf2bb9bc
tuned message;

diff -r 1d6e9048cb62 -r fe6d2cd61009 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Mar 14 18:08:21 2017 +0100
+++ b/src/Pure/General/exn.scala	Tue Mar 14 19:40:39 2017 +0100
@@ -20,7 +20,7 @@
       }
     override def hashCode: Int = message.hashCode
 
-    override def toString: String = "ERROR(" + message + ")"
+    override def toString: String = "ERROR(" + Output.clean_yxml(message) + ")"
   }
 
   object ERROR