#1260 (Aug 19, 2020, 1:46:04 AM)

1. List_Lexorder finally working (detail / hgweb)
2. lexicographic ordering: new simp setup to prioritise the simpler "less_than" case (detail / hgweb)
3. merged (detail / hgweb)
4. fixed for new lex-order. And the effing indentation! (detail / hgweb)
5. merged (detail / hgweb)
6. S Holub's proposed generalisation of the lexicographic product of two orderings (detail / hgweb)

Started by an SCM change

This run spent:

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