src/Tools/jEdit/patches/favorites
2 months ago ago formal update of patches -- no change of content;
3 months ago ago more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";