#1423 (Jan 19, 2018, 10:42:00 PM)

1. merged (detail / hgweb)
2. avoid evaluation of embedded comment; (detail / hgweb)
3. disable "display" style in marginal (line) comment; (detail / hgweb)
4. more uniform output of source / text / theory_text, with handling of formal comments etc.; (detail / hgweb)
5. sort completion result; (detail / hgweb)
6. recovered antiquotation check without latex mode (cf. dfc93f2b01ea); (detail / hgweb)
7. formal treatment of documentation names; (detail / hgweb)
8. support for completion; (detail / hgweb)
9. adapted to a5ca98950a91; (detail / hgweb)
10. tuned output of plain name; (detail / hgweb)
11. clarified signature; (detail / hgweb)
12. tuned; (detail / hgweb)
13. tuned; (detail / hgweb)
14. unused; (detail / hgweb)
15. clarified access to antiquotation options;
    define explicit variants of antiquotations;
    output proper Latex.text;
    misc tuning and clarification; (detail / hgweb)
16. more operations; (detail / hgweb)
17. tuned signature; (detail / hgweb)
18. discontinued unused wrapper: print_mode is provided directly; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 3 sec waiting;
• 5 hr 4 min build duration;
• 5 hr 9 min total from scheduled to completion.