equal
deleted
inserted
replaced
|
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-01-20 20:55:19.968888999 +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 |