#865 (Feb 11, 2019, 12:50:07 AM)

1. more robust: avoid duplicate Socket.close; (detail / hgweb)
2. enable subpixel anti-aliasing by default, assuming that its 4 variants don't make a difference; (detail / hgweb)
3. updated to isabelle_fonts-20190210; (detail / hgweb)
4. recovered missing glyph; (detail / hgweb)
5. auto-hinting of original DejaVu fonts, but not Isabelle symbols; (detail / hgweb)

Started by an SCM change

This run spent:

• 5.4 sec waiting;
• 1 hr 18 min build duration;
• 1 hr 19 min total from scheduled to completion.