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