| changeset 65275 | 50f956a1ac3f |
| parent 65237 | f3ba27dfaeca |
| child 65716 | 678e00851cfb |
--- a/src/Pure/General/exn.scala Wed Mar 15 21:52:04 2017 +0100 +++ b/src/Pure/General/exn.scala Thu Mar 16 11:25:09 2017 +0100 @@ -20,7 +20,7 @@ } override def hashCode: Int = message.hashCode - override def toString: String = Output.error_text(message) + override def toString: String = "\n" + Output.error_text(message) } object ERROR