mathlib3
7c868148 - fix(scripts/remote-install-update-mathlib): try again [ci skip]

Commit
6 years ago
fix(scripts/remote-install-update-mathlib): try again [ci skip] The previous attempt to install setuptools seems to fails for timing reasons (PyGithub need setuptools after it's downloaded but before it is installed, this is probably also a packaging issue in PyGithub).
References
Author
Patrick Massot
Parents
Loading