#1342 (Nov 26, 2020, 12:50:09 AM)

1. merged (detail / hgweb)
2. recovered document output from 6bc199a70bf9; (detail / hgweb)
3. clarified command_timings protocol; (detail / hgweb)
4. more robust: include reports from Thy_Output.present_thy/output_document; (detail / hgweb)
5. more complete report positions, notably for command 'back' (amending eca176f773e0); (detail / hgweb)
6. tuned signature; (detail / hgweb)
7. clarified signature; (detail / hgweb)
8. unused; (detail / hgweb)
9. unused; (detail / hgweb)
10. tuned; (detail / hgweb)
11. removed pointless case: messages should always carry proper position; (detail / hgweb)
12. clarified names; (detail / hgweb)
13. eliminated pointless transaction; (detail / hgweb)
14. tuned signature; (detail / hgweb)
15. clarified document_output vs. progress; (detail / hgweb)
16. clarified: more uniform; (detail / hgweb)
17. more robust; (detail / hgweb)
18. clarified signature and database layout; (detail / hgweb)
19. clarified messages; (detail / hgweb)
20. unused (see ac7ae5067783, 1c451e5c145f); (detail / hgweb)
21. unused; (detail / hgweb)
22. support for PIDE markup in batch build (inactive due to pide_reports=false); (detail / hgweb)
23. clarified signature; (detail / hgweb)
24. proper output of document sources (cf. d892f6d66402); (detail / hgweb)

Started by an SCM change

This run spent:

• 7.9 sec waiting;
• 1 hr 27 min build duration;
• 1 hr 27 min total from scheduled to completion.