proper return code on window close;
authorwenzelm
Sat, 05 Jan 2013 18:36:02 +0100
changeset 50740 21098a577294
parent 50739 5165d7e6d3b9
child 50741 20e6e1a92e54
proper return code on window close;
src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala	Sat Jan 05 17:38:54 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala	Sat Jan 05 18:36:02 2013 +0100
@@ -69,6 +69,8 @@
     private var is_stopped = false
     private var return_code = 0
 
+    override def closeOperation { sys.exit(return_code) }
+
 
     /* text */
 
@@ -127,6 +129,7 @@
         catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
       Swing_Thread.now {
         progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
+        return_code = rc
         button_exit(rc)
       }
     })