changeset 65237 | f3ba27dfaeca |
parent 65235 | fe6d2cd61009 |
child 65275 | 50f956a1ac3f |
--- a/src/Pure/General/exn.scala Tue Mar 14 19:46:53 2017 +0100 +++ b/src/Pure/General/exn.scala Tue Mar 14 20:17:44 2017 +0100 @@ -20,7 +20,7 @@ } override def hashCode: Int = message.hashCode - override def toString: String = "ERROR(" + Output.clean_yxml(message) + ")" + override def toString: String = Output.error_text(message) } object ERROR