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"))