src/Tools/jEdit/patches/vfs_manager
author wenzelm
Tue, 08 Sep 2020 21:14:42 +0200
changeset 72247 c06260b7152c
parent 71932 65fd0f032a75
child 73653 d9823224fcfe
permissions -rw-r--r--
update to official jedit-5.6.0;

diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java	2020-09-03 05:31:03.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2020-09-08 20:13:35.656786460 +0200
@@ -380,6 +380,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