src/Tools/jEdit/src/jEdit.props

--- a/src/Tools/jEdit/src/jEdit.props	Wed Dec 12 14:54:48 2012 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Dec 12 16:28:18 2012 +0100
@@ -205,6 +205,8 @@
 line-end.shortcut=END
 line-home.shortcut=HOME
 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
+plugin.MacOSXPlugin.altDispatcher=true
+plugin.MacOSXPlugin.disableOption=true
 print.font=IsabelleText
 restore.remote=false
 restore=false