#1145 (Mar 15, 2020, 12:50:07 AM)

1. more robust: proper transfer if Context.eq_thy_id; (detail / hgweb)
2. merged (detail / hgweb)
3. tuned; (detail / hgweb)
4. tuned; (detail / hgweb)
5. more robust hg_url;
   clarified signature; (detail / hgweb)
6. proper usage (amending 8c7706b053c7); (detail / hgweb)
7. proper escape for literal single quotes; (detail / hgweb)
8. some uses of "' " as witness for this feature; (detail / hgweb)
9. allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962); (detail / hgweb)
10. tidied up a few little proofs (detail / hgweb)

Started by an SCM change

This run spent:

• 6.5 sec waiting;
• 1 hr 20 min build duration;
• 1 hr 20 min total from scheduled to completion.