-error_exit() {
- echo "$@" >&2
- exit 1
-}
-
-write_gitinfo() {
- git_url=$(git config --get remote.origin.url)
- git_rev=$(git rev-parse HEAD)
- echo "$git_url: $git_rev"
-}
-
-if [ $# -eq 0 ]; then
- OUTPUT_DIR=$(pwd)
-else
- OUTPUT_DIR=$(readlink -f $1)
- shift
-fi
-
-mkdir -p $OUTPUT_DIR || error_exit "Could not create directory $OUTPUT_DIR"
-
-echo "Building armband, output dir: $OUTPUT_DIR"
-cd ..