#1248 (Aug 7, 2020, 1:50:34 AM)

1. merged (detail / hgweb)
2. recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a); (detail / hgweb)
3. more compact command_timings, as in former batch-build; (detail / hgweb)
4. unused; (detail / hgweb)
5. unused --- superseded by PIDE messages; (detail / hgweb)
6. more thorough cleanup, e.g. before ML_Heap.save; (detail / hgweb)
7. discontinued old batch-build functionality; (detail / hgweb)
8. tailored towards remaining essence (detail / hgweb)
9. merged (detail / hgweb)
10. tuned (detail / hgweb)
11. added theory Tree23_of_List (detail / hgweb)
12. more robust treatment of thm_names, with strict check after all theories are loaded; (detail / hgweb)
13. a few more lemmas (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 0 min waiting;
• 1 hr 26 min build duration;
• 2 hr 27 min total from scheduled to completion.