#730 (Sep 9, 2018, 12:50:07 AM)

1. tuned message; (detail / hgweb)
2. more robust test: virtualization may provide misleading information; (detail / hgweb)
3. implicit use of NUMA policy, absorbing potential errors; (detail / hgweb)
4. tuned signature; (detail / hgweb)
5. tuned; (detail / hgweb)
6. more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session; (detail / hgweb)
7. merged (detail / hgweb)
8. ensure foundational order of commits, taking Pure as implicit starting point; (detail / hgweb)
9. more accurate output; (detail / hgweb)
10. clarified defaults;
    more uniform treatment of "disabled" case; (detail / hgweb)
11. more accurate output; (detail / hgweb)
12. support for watchdog_timeout; (detail / hgweb)
13. tuned signature; (detail / hgweb)
14. tuned signature; (detail / hgweb)
15. removed junk; (detail / hgweb)
16. tuned output; (detail / hgweb)
17. more appropriate conversion of HOL character literals to character codes: symbolic newline is interpreted as 0x10 (detail / hgweb)
18. more explicit notion of ord value for HOL characters (detail / hgweb)
19. left-over rename from 3f9bb52082c4 (detail / hgweb)

Started by an SCM change

This run spent:

• 5.5 sec waiting;
• 1 hr 13 min build duration;
• 1 hr 13 min total from scheduled to completion.