--- a/src/Pure/System/system_dialog.scala Sat Sep 07 15:10:33 2013 +0200
+++ b/src/Pure/System/system_dialog.scala Sat Sep 07 15:28:16 2013 +0200
@@ -54,6 +54,7 @@
case None =>
case Some(window) =>
window.visible = false
+ window.dispose
_window = None
}
--- a/src/Pure/Tools/main.scala Sat Sep 07 15:10:33 2013 +0200
+++ b/src/Pure/Tools/main.scala Sat Sep 07 15:28:16 2013 +0200
@@ -36,7 +36,9 @@
def run
{
build
- if (system_dialog.join == 0) start
+ val rc = system_dialog.join
+ if (rc == 0) start
+ else sys.exit(rc)
}
def build