diff options
| author | typebrook <typebrook@gmail.com> | 2020-03-02 21:14:18 +0800 |
|---|---|---|
| committer | typebrook <typebrook@gmail.com> | 2020-03-02 21:14:18 +0800 |
| commit | f99cdfec4b49838ea8517d790e517e93f53ae26f (patch) | |
| tree | 22b66c64b91eebe51bf518a424088d48828addfd /tools | |
| parent | a2497077066d4e26268bdd071851482252e45020 (diff) | |
update
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/install.sh | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/tools/install.sh b/tools/install.sh new file mode 100644 index 0000000..54bcef1 --- /dev/null +++ b/tools/install.sh | |||
| @@ -0,0 +1,16 @@ | |||
| 1 | #! /usr/bin/env bash | ||
| 2 | |||
| 3 | set -e | ||
| 4 | |||
| 5 | # Default settings | ||
| 6 | SETTING_DIR=${SETTING_DIR:-~/settings} | ||
| 7 | REPO=${REPO:-typebrook/settings} | ||
| 8 | REMOTE=${REMOTE:-https://github.com/${REPO}.git} | ||
| 9 | BRANCH=${BRANCH:-master} | ||
| 10 | |||
| 11 | git clone --depth=1 --branch "$BRANCH" "$REMOTE" "$SETTING_DIR" || { | ||
| 12 | error "git clone of settings repo failed" | ||
| 13 | exit 1 | ||
| 14 | } | ||
| 15 | |||
| 16 | cd "$SETTING_DIR" && make | ||