#1446 (Feb 1, 2018, 9:19:04 PM)

1. tuned: more standard use of order; (detail / hgweb)
2. tuned; (detail / hgweb)
3. tuned; (detail / hgweb)
4. clarified signature;
   eliminated aliases of Thm.term_ord; (detail / hgweb)
5. clarified signature: prefer proper order operation; (detail / hgweb)
6. tuned signature: more operations; (detail / hgweb)
7. clarified signature; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 0 sec waiting;
• 3 hr 19 min build duration;
• 3 hr 24 min total from scheduled to completion.