author | wenzelm |
Sat, 07 Sep 2013 17:43:13 +0200 | |
changeset 53462 | c531db093680 |
parent 53461 | 26c609ada983 |
child 53463 | 7863f4b3b73b |
--- a/src/Pure/Tools/main.scala Sat Sep 07 17:32:55 2013 +0200 +++ b/src/Pure/Tools/main.scala Sat Sep 07 17:43:13 2013 +0200 @@ -132,6 +132,11 @@ } } catch { case exn: Throwable => exit_error(exn) } + + if (system_dialog.stopped) { + system_dialog.return_code(130) + system_dialog.join_exit + } } build