#875 (Feb 25, 2019, 12:50:10 AM)

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

Started by an SCM change

This run spent:

• 8.7 sec waiting;
• 1 hr 27 min build duration;
• 1 hr 28 min total from scheduled to completion.