--- a/src/Tools/jEdit/patches/jedit/macos Wed Sep 25 20:28:49 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 2013-07-28 19:03:49.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2013-09-05 10:55:36.388181955 +0200
-@@ -109,7 +109,7 @@
- * used to handle a modifier key press in conjunction with an alphabet
- * key. <b>On by default on MacOS.</b>
- */
-- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
-+ public static boolean ALTERNATIVE_DISPATCHER = false;
-
- /**
- * If true, A+ shortcuts are disabled. If you use this, you should also
-