src/Tools/jEdit/patches/vfs_manager
author wenzelm
Wed, 20 Dec 2023 11:55:04 +0100
changeset 79316 7464bb64622d
parent 73653 d9823224fcfe
child 81297 07f64697408e
permissions -rw-r--r--
clarified ML toplevel output: avoid "??." prefix;

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