Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(scripts/remote-install-update-mathlib): missing dependency
Also add a `--upgrade` option to `pip install` in case something is already there but outdated
- Loading branch information