src/Pure/Tools/main.scala
changeset 56782 433cf57550fa
parent 56671 06853449cf0a
child 56890 7f120d227ca5
--- a/src/Pure/Tools/main.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/Tools/main.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -61,7 +61,8 @@
                     system_mode = system_mode, sessions = List(session)))
               }
               catch {
-                case exn: Throwable => (Exn.error_message(exn) + "\n", Exn.return_code(exn, 2))
+                case exn: Throwable =>
+                  (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
               }
 
             system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))