# HG changeset patch # User wenzelm # Date 1548968570 -3600 # Node ID a2218981a5d698d3a73d49d10c23a2aaded3a110 # Parent 09ad02c0fbeefa694111621cfefa2d2c9e87cb7a more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME"; diff -r 09ad02c0fbee -r a2218981a5d6 src/Tools/jEdit/patches/favorites --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/favorites Thu Jan 31 22:02:50 2019 +0100 @@ -0,0 +1,13 @@ +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/FavoritesVFS.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java +--- 5.5.0/jEdit/org/gjt/sp/jedit/io/FavoritesVFS.java 2018-04-09 01:57:13.000000000 +0200 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java 2019-01-31 21:48:47.418367799 +0100 +@@ -70,7 +70,8 @@ + public VFSFile[] _listFiles(Object session, String url, + Component comp) + { +- return getFavorites(); ++ if (url.equals(PROTOCOL + ':')) return getFavorites(); ++ else return null; + } //}}} + + //{{{ _getFile() method