#539 (Jan 27, 2018, 12:50:10 AM)

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

Started by an SCM change

This run spent:

• 7.6 sec waiting;
• 1 hr 15 min build duration;
• 1 hr 15 min total from scheduled to completion.