diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/folding --- a/src/Tools/jEdit/patches/folding Fri Oct 23 18:39:14 2015 +0200 +++ b/src/Tools/jEdit/patches/folding Fri Oct 23 21:03:16 2015 +0200 @@ -1,7 +1,7 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-02-02 02:14:26.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-02-28 20:55:39.932158194 +0100 -@@ -1936,29 +1936,23 @@ +diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java +--- 5.3.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-10-20 19:56:02.000000000 +0200 ++++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-10-23 20:02:38.897330618 +0200 +@@ -1956,29 +1956,23 @@ { Segment seg = new Segment(); newFoldLevel = foldHandler.getFoldLevel(this,i,seg);