src/Tools/jEdit/patches/vfs_manager
changeset 81297 07f64697408e
parent 73653 d9823224fcfe
--- a/src/Tools/jEdit/patches/vfs_manager	Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/vfs_manager	Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2020-09-03 05:31:03.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2021-05-10 11:02:05.808257746 +0200
-@@ -380,6 +380,18 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2024-10-29 11:50:54.062016616 +0100
+@@ -339,6 +339,18 @@
  
  				if(vfsUpdates.size() == 1)
  				{