# HG changeset patch
# User wenzelm
# Date 1358428355 -3600
# Node ID e424e17ee42048e7f505ba09c5d29efc91982a14
# Parent  7f0bc95af61c30f8f410076450ef9a1f74dddeb5# Parent  ca071373b695ae266a6c7f6b8d62bd2a0b50018d
merged

diff -r 7f0bc95af61c -r e424e17ee420 Admin/lib/Tools/components_checksum
--- a/Admin/lib/Tools/components_checksum	Thu Jan 17 14:06:14 2013 +0100
+++ b/Admin/lib/Tools/components_checksum	Thu Jan 17 14:12:35 2013 +0100
@@ -71,11 +71,10 @@
 
 (
   cd "$COMPONENTS_DIR"
-  sha1sum *.tar.gz > "$CHECKSUM_TMP"
+  sha1sum *.tar.gz | sort -k2 > "$CHECKSUM_TMP"
 )
 
 [ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE"
 [ -n "$CHECK" ] && {
   diff "$CHECKSUM_FILE" "$CHECKSUM_TMP" || fail "Integrity error"
 }
-
diff -r 7f0bc95af61c -r e424e17ee420 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Jan 17 14:06:14 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Jan 17 14:12:35 2013 +0100
@@ -439,8 +439,10 @@
 
 fun error_msg pos ((serial, msg), exec_id) =
   Position.setmp_thread_data pos (fn () =>
-    if is_none exec_id orelse exec_id = Position.get_id pos
-    then Output.error_msg' (serial, msg) else warning msg) ();
+    let val id = Position.get_id pos in
+      if is_none id orelse is_none exec_id orelse id = exec_id
+      then Output.error_msg' (serial, msg) else ()
+    end) ();
 
 fun identify_result pos res =
   (case res of
diff -r 7f0bc95af61c -r e424e17ee420 src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala	Thu Jan 17 14:06:14 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala	Thu Jan 17 14:12:35 2013 +0100
@@ -120,13 +120,15 @@
     val button = new Button("Cancel") {
       reactions += { case ButtonClicked(_) => button_action() }
     }
-    def button_exit()
-    {
-      check_auto_close()
-      button.text = if (return_code == 0) "OK" else "Exit"
-      button_action = (() => sys.exit(return_code))
-      button.peer.getRootPane.setDefaultButton(button.peer)
-    }
+
+    val delay_button_exit =
+      Swing_Thread.delay_first(Time.seconds(1.0))
+      {
+        check_auto_close()
+        button.text = if (return_code == 0) "OK" else "Exit"
+        button_action = (() => sys.exit(return_code))
+        button.peer.getRootPane.setDefaultButton(button.peer)
+      }
 
 
     val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button, auto_close)
@@ -157,7 +159,7 @@
       Swing_Thread.now {
         progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
         return_code = rc
-        button_exit()
+        delay_button_exit.invoke()
       }
     })
   }