#1432 (Jan 26, 2018, 11:58:06 AM)

1. allow cartouche within ML string; (detail / hgweb)
2. verbatim output consists of plain lines; (detail / hgweb)
3. old-style inner comments are legacy; (detail / hgweb)
4. more markup: disable spell-checker for raw latex; (detail / hgweb)
5. clarified signature: items with \isasep are special; (detail / hgweb)
6. clarified signature; (detail / hgweb)
7. tuned message; (detail / hgweb)
8. clarified operations; (detail / hgweb)
9. tuned signature: removed unused operations; (detail / hgweb)
10. tuned: prefer list operations over Source.source;
    approximative parsing of theory header; (detail / hgweb)
11. tuned: prefer list operations over Source.source; (detail / hgweb)
12. tuned: prefer list operations over Source.source; (detail / hgweb)
13. clarified signature; (detail / hgweb)
14. clarified position; (detail / hgweb)
15. clarified operations; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 2 sec waiting;
• 3 hr 21 min build duration;
• 3 hr 26 min total from scheduled to completion.