#2202 (Jun 9, 2024, 12:50:09 AM)

1. renamed lemmas (detail / hgweb)
2. build manager: echo error messages to server output; (detail / hgweb)
3. omit showing previous failures for user builds; (detail / hgweb)
4. always handle interrupted jobs; (detail / hgweb)
5. add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware; (detail / hgweb)
6. clarified context: operations now in build process; (detail / hgweb)
7. clarified: add explicit build process; (detail / hgweb)
8. remove unnecessary subdir; (detail / hgweb)
9. tuned; (detail / hgweb)

Started by an SCM change

This run spent:

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