src/Tools/jEdit/patches/vfs_manager
changeset 69696 9fd395ff57bc
child 69838 4419d4d675c3
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/vfs_manager	Sun Jan 20 21:26:15 2019 +0100
@@ -0,0 +1,22 @@
+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
+--- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2018-04-09 01:57:13.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2019-01-20 20:55:19.968888999 +0100
+@@ -345,6 +345,18 @@
+ 
+ 				if(vfsUpdates.size() == 1)
+ 				{
++					// slowdown race concerning Buffer.isLoading() status
++					// of Buffer.save() + Buffer.finishSaving()
++					// versus Buffer.load() + "runnable"
++					try
++					{
++						Thread.sleep(100);
++					}
++					catch(InterruptedException ie)
++					{
++						Thread.currentThread().interrupt();
++					}
++
+ 					// we were the first to add an update;
+ 					// add update sending runnable to AWT
+ 					// thread