src/Tools/jEdit/patches/favorites
author wenzelm
Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 69838 4419d4d675c3
permissions -rw-r--r--
tuned NEWS;

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-02-24 12:20:21.702501903 +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