Changes

Summary

1. clarified signature, notably for hol4isabelle (by Fabian Immler);
2. updated to jedit_build-20190224 (new patches: favorites, glyphvector);
3. fallback on createGlyphVector for multi-character glyphs (e.g. 0x01d49c), as seen in Java 11;
4. formal update of patches -- no change of content;
5. removed junk;