# HG changeset patch
# User wenzelm
# Date 1357407362 -3600
# Node ID 21098a5772942a5fa6373cf77ba1cd7fd9b9504b
# Parent  5165d7e6d3b9e696654e6cdc4ce89d33c48f0870
proper return code on window close;

diff -r 5165d7e6d3b9 -r 21098a577294 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)
       }
     })