# HG changeset patch
# User wenzelm
# Date 1445981598 -3600
# Node ID 4108f91ca8105af80507735ca3ac6646d3b48ccc
# Parent  9c6346319eeeca65977524fd39a5a2f3e0388b5f
workaround for problem with C-1, C-2, C-3 seen on Slovak QWERTY keyboard;

diff -r 9c6346319eee -r 4108f91ca810 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue Oct 27 22:19:56 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Tue Oct 27 22:33:18 2015 +0100
@@ -1807,6 +1807,14 @@
   Shortcuts\<close> according to national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close>
   on English ones.
 
+  \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic
+  national keyboards may cause a conflict of menu accelerator keys with
+  regular jEdit key bindings. This leads to duplicate execution of the
+  corresponding jEdit action.
+
+  \<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option
+  \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.
+
   \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to
   character drop-outs in the main text area.