From 814cb034fbbfe4797aa1bee0a7ed338d962a9e6f Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Fri, 8 Feb 2019 17:01:30 -0500 Subject: [PATCH] build(update-mathlib): fix installation and documentation --- README.md | 2 +- scripts/remote-install-update-mathlib.sh | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 scripts/remote-install-update-mathlib.sh diff --git a/README.md b/README.md index 649ab306f49f9..9672f7b107f2f 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,7 @@ not specific to mathlib. ## Obtaining binaries -### Install the `update-mathlib` +### Install the `update-mathlib` script *Linux/OS X/Cygwin/MSYS2/git bash*: run the following command in a terminal: diff --git a/scripts/remote-install-update-mathlib.sh b/scripts/remote-install-update-mathlib.sh new file mode 100644 index 0000000000000..381ca5135820b --- /dev/null +++ b/scripts/remote-install-update-mathlib.sh @@ -0,0 +1,5 @@ +#! /bin/sh +pip3 install toml PyGithub urllib3 certifi +curl -o update-mathlib.py https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/update-mathlib.py +chmod +x update-mathlib.py +mv update-mathlib.py /usr/local/bin/update-mathlib