# HG changeset patch
# User wenzelm
# Date 1355326098 -3600
# Node ID 8d8e882c7fbe8fe8135527340d1e1689bfaa70bb
# Parent  0faaa279faee2eaf02b29b8ef92a2b4714cfabf7
prevent dedicated MacOSX plugin from switching off vital workarounds;

diff -r 0faaa279faee -r 8d8e882c7fbe 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