formal update of patches -- no change of content;
authorwenzelm
Sun Feb 24 12:49:32 2019 +0100 (7 weeks ago ago)
changeset 700194419d4d675c3
parent 70018 f2e4a94d9aaf
child 70020 828f3cd0dcf9
formal update of patches -- no change of content;
src/Tools/jEdit/patches/accelerator_font
src/Tools/jEdit/patches/docking
src/Tools/jEdit/patches/extended_styles
src/Tools/jEdit/patches/favorites
src/Tools/jEdit/patches/folding
src/Tools/jEdit/patches/props
src/Tools/jEdit/patches/putenv
src/Tools/jEdit/patches/title
src/Tools/jEdit/patches/vfs_manager
src/Tools/jEdit/patches/vfs_marker
     1.1 --- a/src/Tools/jEdit/patches/accelerator_font	Sun Feb 24 12:48:43 2019 +0100
     1.2 +++ b/src/Tools/jEdit/patches/accelerator_font	Sun Feb 24 12:49:32 2019 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
     1.5 ---- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2018-12-01 15:51:30.320182833 +0100
     1.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java	2018-12-01 15:51:49.028286932 +0100
     1.7 +--- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2018-04-09 01:58:07.000000000 +0200
     1.8 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java	2019-02-24 12:19:52.134389619 +0100
     1.9  @@ -1172,7 +1172,7 @@
    1.10   				return new Font("Monospaced", Font.PLAIN, 12);
    1.11   			}
     2.1 --- a/src/Tools/jEdit/patches/docking	Sun Feb 24 12:48:43 2019 +0100
     2.2 +++ b/src/Tools/jEdit/patches/docking	Sun Feb 24 12:49:32 2019 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
     2.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2018-04-09 01:56:46.000000000 +0200
     2.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2018-04-17 13:57:40.320348370 +0200
     2.7 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2019-02-24 12:20:02.862430679 +0100
     2.8  @@ -35,7 +35,7 @@
     2.9   import javax.swing.Box;
    2.10   import javax.swing.BoxLayout;
     3.1 --- a/src/Tools/jEdit/patches/extended_styles	Sun Feb 24 12:48:43 2019 +0100
     3.2 +++ b/src/Tools/jEdit/patches/extended_styles	Sun Feb 24 12:49:32 2019 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
     3.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2018-04-09 01:57:24.000000000 +0200
     3.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2018-04-17 13:58:12.912465088 +0200
     3.7 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2019-02-24 12:32:09.336643045 +0100
     3.8  @@ -322,9 +322,9 @@
     3.9   	//{{{ Package private members
    3.10   
    3.11 @@ -24,7 +24,7 @@
    3.12   
    3.13  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
    3.14  --- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-09 01:58:01.000000000 +0200
    3.15 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-17 13:58:12.912465088 +0200
    3.16 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2019-02-24 12:20:10.550459878 +0100
    3.17  @@ -917,6 +917,11 @@
    3.18   		return chunkCache.getLineInfo(screenLine).physicalLine;
    3.19   	} //}}}
    3.20 @@ -39,7 +39,7 @@
    3.21   	 * Returns the screen (wrapped) line containing the specified offset.
    3.22  diff -ru 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    3.23  --- 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2018-04-09 01:58:37.000000000 +0200
    3.24 -+++ 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2018-04-17 13:58:12.912465088 +0200
    3.25 ++++ 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2019-02-24 12:20:10.550459878 +0100
    3.26  @@ -200,7 +200,24 @@
    3.27   	{
    3.28   		return loadStyles(family,size,true);
     4.1 --- a/src/Tools/jEdit/patches/favorites	Sun Feb 24 12:48:43 2019 +0100
     4.2 +++ b/src/Tools/jEdit/patches/favorites	Sun Feb 24 12:49:32 2019 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/FavoritesVFS.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java
     4.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/io/FavoritesVFS.java	2018-04-09 01:57:13.000000000 +0200
     4.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java	2019-01-31 21:48:47.418367799 +0100
     4.7 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java	2019-02-24 12:20:21.702501903 +0100
     4.8  @@ -70,7 +70,8 @@
     4.9   	public VFSFile[] _listFiles(Object session, String url,
    4.10   		Component comp)
     5.1 --- a/src/Tools/jEdit/patches/folding	Sun Feb 24 12:48:43 2019 +0100
     5.2 +++ b/src/Tools/jEdit/patches/folding	Sun Feb 24 12:49:32 2019 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4  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
     5.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2018-04-09 01:57:06.000000000 +0200
     5.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2018-04-17 13:58:42.984572359 +0200
     5.7 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2019-02-24 12:20:30.594535134 +0100
     5.8  @@ -1961,29 +1961,23 @@
     5.9   			{
    5.10   				Segment seg = new Segment();
     6.1 --- a/src/Tools/jEdit/patches/props	Sun Feb 24 12:48:43 2019 +0100
     6.2 +++ b/src/Tools/jEdit/patches/props	Sun Feb 24 12:49:32 2019 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4  diff -ru 5.5.0/jEdit/org/jedit/localization/jedit_en.props 5.5.0/jEdit-patched/org/jedit/localization/jedit_en.props
     6.5  --- 5.5.0/jEdit/org/jedit/localization/jedit_en.props	2018-04-09 01:58:42.000000000 +0200
     6.6 -+++ 5.5.0/jEdit-patched/org/jedit/localization/jedit_en.props	2018-04-17 13:59:10.688670850 +0200
     6.7 ++++ 5.5.0/jEdit-patched/org/jedit/localization/jedit_en.props	2019-02-24 12:21:02.506652445 +0100
     6.8  @@ -1270,8 +1270,7 @@
     6.9   	The most likely reason is that the JAR file is corrupt; try\n\
    6.10   	reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
     7.1 --- a/src/Tools/jEdit/patches/putenv	Sun Feb 24 12:48:43 2019 +0100
     7.2 +++ b/src/Tools/jEdit/patches/putenv	Sun Feb 24 12:49:32 2019 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
     7.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2018-04-09 01:57:06.000000000 +0200
     7.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2018-10-26 12:29:44.315185808 +0200
     7.7 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2019-02-24 12:21:09.602678130 +0100
     7.8  @@ -126,6 +126,21 @@
     7.9   	static final Pattern winPattern = Pattern.compile(winPatternString);
    7.10   
     8.1 --- a/src/Tools/jEdit/patches/title	Sun Feb 24 12:48:43 2019 +0100
     8.2 +++ b/src/Tools/jEdit/patches/title	Sun Feb 24 12:49:32 2019 +0100
     8.3 @@ -1,6 +1,6 @@
     8.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/View.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java
     8.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/View.java	2018-04-09 01:57:31.000000000 +0200
     8.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java	2018-05-04 21:18:11.891194939 +0200
     8.7 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java	2019-02-24 12:21:17.050704937 +0100
     8.8  @@ -1233,15 +1233,10 @@
     8.9   
    8.10   		StringBuilder title = new StringBuilder();
     9.1 --- a/src/Tools/jEdit/patches/vfs_manager	Sun Feb 24 12:48:43 2019 +0100
     9.2 +++ b/src/Tools/jEdit/patches/vfs_manager	Sun Feb 24 12:49:32 2019 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
     9.5  --- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2018-04-09 01:57:13.000000000 +0200
     9.6 -+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2019-01-20 20:55:19.968888999 +0100
     9.7 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2019-02-24 12:21:25.986736893 +0100
     9.8  @@ -345,6 +345,18 @@
     9.9   
    9.10   				if(vfsUpdates.size() == 1)
    10.1 --- a/src/Tools/jEdit/patches/vfs_marker	Sun Feb 24 12:48:43 2019 +0100
    10.2 +++ b/src/Tools/jEdit/patches/vfs_marker	Sun Feb 24 12:49:32 2019 +0100
    10.3 @@ -1,6 +1,6 @@
    10.4 -diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
    10.5 ---- jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java	2018-04-09 01:57:42.000000000 +0200
    10.6 -+++ jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2019-01-30 22:18:22.534820468 +0100
    10.7 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
    10.8 +--- 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java	2018-04-09 01:57:42.000000000 +0200
    10.9 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2019-02-24 12:23:42.403199825 +0100
   10.10  @@ -1204,6 +1204,7 @@
   10.11   		VFSFile[] selectedFiles = browserView.getSelectedFiles();
   10.12   
   10.13 @@ -53,9 +53,9 @@
   10.14   		}
   10.15   
   10.16   		Object[] listeners = listenerList.getListenerList();
   10.17 -diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
   10.18 ---- jEdit/org/gjt/sp/jedit/io/VFSFile.java	2018-04-09 01:57:13.000000000 +0200
   10.19 -+++ jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2019-01-30 21:55:19.531911500 +0100
   10.20 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
   10.21 +--- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java	2018-04-09 01:57:13.000000000 +0200
   10.22 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2019-02-24 12:23:42.403199825 +0100
   10.23  @@ -297,6 +297,12 @@
   10.24   		}
   10.25   	} //}}}
   10.26 @@ -70,8 +70,8 @@
   10.27   	public String getPath()
   10.28   	{
   10.29  diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
   10.30 ---- jEdit/org/gjt/sp/jedit/jEdit.java	2018-04-09 01:56:22.000000000 +0200
   10.31 -+++ jEdit-patched/org/gjt/sp/jedit/jEdit.java	2019-01-30 21:56:00.171827173 +0100
   10.32 +--- 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java	2018-04-09 01:56:22.000000000 +0200
   10.33 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2019-02-24 12:23:42.403199825 +0100
   10.34  @@ -4479,7 +4479,7 @@
   10.35   	} //}}}
   10.36