Skip to content

Commit

Permalink
fix(scripts/remote-install-update-mathlib): add GitPython dependency
Browse files Browse the repository at this point in the history
  • Loading branch information
bryangingechen committed Mar 29, 2019
1 parent 2e7f009 commit 7cc6ceb
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/remote-install-update-mathlib.sh
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#! /bin/sh
echo "Installing python dependencies (at user level)"
pip3 install --user toml PyGithub urllib3 certifi
pip3 install --user toml PyGithub urllib3 certifi GitPython
echo "Fetching the update-mathlib script"
curl -o update-mathlib.py https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/update-mathlib.py
echo "installing it in \$HOME/.mathlib/bin"
Expand Down

0 comments on commit 7cc6ceb

Please sign in to comment.