#1022 (May 27, 2024, 1:45:42 PM)

1. sledgehammer pretty-printing: merge x(1) x(2) to x(1,2) (detail / hgweb)
2. tuned; (detail / hgweb)
3. tuned spelling; (detail / hgweb)
4. support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs"); (detail / hgweb)
5. clarified signature; (detail / hgweb)
6. more general dirs for Sync.sync; (detail / hgweb)
7. tuned whitespace (amending beb4ee344c22); (detail / hgweb)
8. clarified signature (see also be0ab4b94c62 and c41791ad75c3); (detail / hgweb)
9. tuned; (detail / hgweb)
10. clarified signature; (detail / hgweb)
11. tuned names; (detail / hgweb)
12. proper SSH.System operation; (detail / hgweb)
13. clarified modules; (detail / hgweb)
14. more uniform/robust detect_repository/is_repository: actually check hg root; (detail / hgweb)
15. more uniform local/remote operations; (detail / hgweb)

Started by an SCM change

This run spent:

• 9.7 sec waiting;
• 24 min build duration;
• 24 min total from scheduled to completion.

• Isabelle_Marries_Dirac
• ML_Unification
• Proof_Strategy_Language
• Frequency_Moments