# HG changeset patch
# User wenzelm
# Date 1378560496 -7200
# Node ID b7c15885fd1e9c51df97870bddb7780a298ac315
# Parent  d12be8f6228500387d605a7440a986c5975ee9cc
more robust exit;

diff -r d12be8f62285 -r b7c15885fd1e src/Pure/System/system_dialog.scala
--- 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
     }
 
diff -r d12be8f62285 -r b7c15885fd1e src/Pure/Tools/main.scala
--- 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