#1870 (Jan 24, 2023, 12:50:09 AM)

1. merged (detail / hgweb)
2. support remote operations; (detail / hgweb)
3. more elementary command-line, following lib/Tools/components; (detail / hgweb)
4. clarified defaults;
   proper Url.append_path; (detail / hgweb)
5. more accurate options (amending 7e19dc018db9); (detail / hgweb)
6. clarified defaults; (detail / hgweb)
7. support remote download_file; (detail / hgweb)
8. more modular shell script; (detail / hgweb)
9. more uniform options for "curl", following lib/Tools/components; (detail / hgweb)
10. tuned: drop redundant "expand"; (detail / hgweb)
11. tuned; (detail / hgweb)
12. added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp (detail / hgweb)
13. proper name for lemma totalp_on_total_on_eq (detail / hgweb)

Started by an SCM change

This run spent:

• 8.5 sec waiting;
• 1 hr 52 min build duration;
• 1 hr 52 min total from scheduled to completion.