src/Tools/jEdit/patches/vfs_manager
author wenzelm
Fri, 26 Apr 2024 13:25:44 +0200
changeset 80150 96f60533ec1d
parent 73653 d9823224fcfe
permissions -rw-r--r--
update Windows test machines;

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 @@
 
 				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