src/Tools/jEdit/patches/vfs_manager
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 69711 9fd395ff57bc
permissions -rw-r--r--
formal update of patches -- no change of content;
     1 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
     2 --- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2018-04-09 01:57:13.000000000 +0200
     3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2019-02-24 12:21:25.986736893 +0100
     4 @@ -345,6 +345,18 @@
     5  
     6  				if(vfsUpdates.size() == 1)
     7  				{
     8 +					// slowdown race concerning Buffer.isLoading() status
     9 +					// of Buffer.save() + Buffer.finishSaving()
    10 +					// versus Buffer.load() + "runnable"
    11 +					try
    12 +					{
    13 +						Thread.sleep(100);
    14 +					}
    15 +					catch(InterruptedException ie)
    16 +					{
    17 +						Thread.currentThread().interrupt();
    18 +					}
    19 +
    20  					// we were the first to add an update;
    21  					// add update sending runnable to AWT
    22  					// thread