# HG changeset patch
# User wenzelm
# Date 1472744117 -7200
# Node ID 23b013b6b2fb8b9f6b880ec6adde5c0fa4c1ace1
# Parent  c57db6b2befc4b9abae3ecdcf04b1c3dcf8afd68
tuned GUI: modal dialog last;

diff -r c57db6b2befc -r 23b013b6b2fb src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 17:35:01 2016 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 17:35:17 2016 +0200
@@ -333,9 +333,9 @@
               "It is for testing only, not for production use.")
           }
 
-          Keymap_Merge.check_dialog(jEdit.getActiveView())
+          Session_Build.session_build(jEdit.getActiveView())
 
-          Session_Build.session_build(jEdit.getActiveView())
+          Keymap_Merge.check_dialog(jEdit.getActiveView())
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED ||