author | wenzelm |
Tue, 14 Mar 2017 19:40:39 +0100 | |
changeset 65235 | fe6d2cd61009 |
parent 65234 | 1d6e9048cb62 |
child 65236 | 4fa82bbb394e |
--- 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