src/Tools/jEdit/patches/folding
changeset 67993 752a4e6d760c
parent 65329 4f3da52cec02
child 70019 4419d4d675c3
     1.1 --- a/src/Tools/jEdit/patches/folding	Tue Apr 17 10:22:42 2018 +0100
     1.2 +++ b/src/Tools/jEdit/patches/folding	Tue Apr 17 14:48:55 2018 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4 -diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
     1.5 ---- 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java	2017-03-18 14:30:28.000000000 +0100
     1.6 -+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2017-03-19 19:27:45.734945702 +0100
     1.7 -@@ -1950,29 +1950,23 @@
     1.8 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
     1.9 +--- 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2018-04-09 01:57:06.000000000 +0200
    1.10 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2018-04-17 13:58:42.984572359 +0200
    1.11 +@@ -1961,29 +1961,23 @@
    1.12   			{
    1.13   				Segment seg = new Segment();
    1.14   				newFoldLevel = foldHandler.getFoldLevel(this,i,seg);