diff -r 346acc4b05c0 -r 427724cff970 src/Tools/jEdit/patches/jedit/brackets --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/jedit/brackets Wed Aug 21 22:40:55 2013 +0200 @@ -0,0 +1,15 @@ +diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java +--- 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2012-11-17 16:42:29.000000000 +0100 ++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-08-21 22:13:10.688736361 +0200 +@@ -97,6 +97,10 @@ + 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'; + } + } //}}} +