#717 (Aug 26, 2018, 12:50:08 AM)

1. merged (detail / hgweb)
2. material on finite maps (detail / hgweb)
3. more uniform cartouche syntax;
   more documentation; (detail / hgweb)
4. more uniform cartouche syntax; (detail / hgweb)
5. more robust exit: avoid later Consolidate_Execution with handle_raw_edits (cf. 2fd3a6d6ba2e); (detail / hgweb)
6. tuned message; (detail / hgweb)
7. clarified message; (detail / hgweb)
8. actually ensure globally unique counter results (amending a5853334c179); (detail / hgweb)
9. retain original PolyML.pointerEq; (detail / hgweb)
10. some modernization of notation (detail / hgweb)
11. deprecation of ASCII syntax for indexed big operators (detail / hgweb)

Started by an SCM change

This run spent:

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