#528 (Jan 14, 2018, 12:50:09 AM)

1. added glyph from "Deja Vu Sans Mono" font; (detail / hgweb)
2. tuned messages; (detail / hgweb)
3. merged (detail / hgweb)
4. allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1); (detail / hgweb)
5. tuned; (detail / hgweb)
6. tuned; (detail / hgweb)
7. more general error suffixes, e.g. for messages that are broken over several lines; (detail / hgweb)
8. another Latex error seen in the wild:
   Undefined control sequence.
   \isamarkupcancel #1->\xout (detail / hgweb)
9. clarified default; (detail / hgweb)
10. clarified formal comments; (detail / hgweb)
11. prefer formal comments; (detail / hgweb)
12. added \<^cancel> operator for unused text; (detail / hgweb)
13. tuned; (detail / hgweb)
14. restored naming of lemmas after corresponding constants (detail / hgweb)

Started by an SCM change

This run spent:

• 7.3 sec waiting;
• 1 hr 22 min build duration;
• 1 hr 22 min total from scheduled to completion.