| 1234567891011121314151617181920212223242526272829 |
- #!/bin/bash
- set -e
- pushd $(cd $(dirname ${0})/..; pwd) > /dev/null
- bold() {
- echo "$(tty -s && tput bold)$1$(tty -s && tput sgr0)"
- }
- clean() {
- bold "torch clean"
- rm -rf "./third_party/src/torch"
- }
- sync() {
- bold "torch sync"
- [ -d "./third_party/src/torch" ] || git clone --quiet https://github.com/torch/torch7.git "./third_party/src/torch"
- pushd "./third_party/src/torch" > /dev/null
- git pull --quiet --prune
- popd > /dev/null
- }
- while [ "$#" != 0 ]; do
- command="$1" && shift
- case "${command}" in
- "clean") clean;;
- "sync") sync;;
- esac
- done
|