--- a/src/Tools/jEdit/patches/jedit/brackets Wed Sep 25 20:28:49 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2013-07-28 19:03:24.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-09-05 10:51:09.996193290 +0200
-@@ -97,6 +97,22 @@
- case '}': if (direction != null) direction[0] = false; return '{';
- case '<': if (direction != null) direction[0] = true; return '>';
- case '>': if (direction != null) direction[0] = false; return '<';
-+ case '«': if (direction != null) direction[0] = true; return '»';
-+ case '»': if (direction != null) direction[0] = false; return '«';
-+ case '‹': if (direction != null) direction[0] = true; return '›';
-+ case '›': if (direction != null) direction[0] = false; return '‹';
-+ case '⟨': if (direction != null) direction[0] = true; return '⟩';
-+ case '⟩': if (direction != null) direction[0] = false; return '⟨';
-+ case '⌈': if (direction != null) direction[0] = true; return '⌉';
-+ case '⌉': if (direction != null) direction[0] = false; return '⌈';
-+ case '⌊': if (direction != null) direction[0] = true; return '⌋';
-+ case '⌋': if (direction != null) direction[0] = false; return '⌊';
-+ case '⦇': if (direction != null) direction[0] = true; return '⦈';
-+ case '⦈': if (direction != null) direction[0] = false; return '⦇';
-+ case '⟦': if (direction != null) direction[0] = true; return '⟧';
-+ case '⟧': if (direction != null) direction[0] = false; return '⟦';
-+ case '⦃': if (direction != null) direction[0] = true; return '⦄';
-+ case '⦄': if (direction != null) direction[0] = false; return '⦃';
- default: return '\0';
- }
- } //}}}