Skip to content

Commit

Permalink
fix(scripts/remote-install-update-mathlib): missing dependency
Browse files Browse the repository at this point in the history
Also add a `--upgrade` option to `pip install` in case something is
already there but outdated
  • Loading branch information
Patrick Massot committed Apr 30, 2019
1 parent 8dcce05 commit e7f68cd
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions scripts/remote-install-update-mathlib.sh
Expand Up @@ -2,7 +2,7 @@
BRANCH=master
USER="--user"
USER_MSG="(at user level)"
PYTHON_DEPS="toml PyGithub urllib3 certifi gitpython"
PYTHON_DEPS="setuptools toml PyGithub urllib3 certifi gitpython"

for i in "$@"
do
Expand Down Expand Up @@ -54,7 +54,7 @@ if ! which pip3; then
fi
fi

pip3 install $USER $PYTHON_DEPS || exit -1
pip3 install --upgrade $USER $PYTHON_DEPS || exit -1
echo "Fetching the update-mathlib script"
curl -o update-mathlib.py https://raw.githubusercontent.com/leanprover-community/mathlib/$BRANCH/scripts/update-mathlib.py
curl -o cache-olean.py https://raw.githubusercontent.com/leanprover-community/mathlib/$BRANCH/scripts/cache-olean.py
Expand Down

0 comments on commit e7f68cd

Please sign in to comment.