author | wenzelm |
Sun, 24 Feb 2019 12:49:32 +0100 | |
changeset 69838 | 4419d4d675c3 |
parent 69779 | a2218981a5d6 |
permissions | -rw-r--r-- |
69779
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
1 |
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 |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
2 |
--- 5.5.0/jEdit/org/gjt/sp/jedit/io/FavoritesVFS.java 2018-04-09 01:57:13.000000000 +0200 |
69838
4419d4d675c3
formal update of patches -- no change of content;
wenzelm
parents:
69779
diff
changeset
|
3 |
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java 2019-02-24 12:20:21.702501903 +0100 |
69779
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
4 |
@@ -70,7 +70,8 @@ |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
5 |
public VFSFile[] _listFiles(Object session, String url, |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
6 |
Component comp) |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
7 |
{ |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
8 |
- return getFavorites(); |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
9 |
+ if (url.equals(PROTOCOL + ':')) return getFavorites(); |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
10 |
+ else return null; |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
11 |
} //}}} |
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
12 |
|
a2218981a5d6
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
wenzelm
parents:
diff
changeset
|
13 |
//{{{ _getFile() method |