website: bootstrap.sh should recommend adding .jiri_root/scripts to PATH
JIRI_ROOT/devtools/bin will be deperated at some point, and we are
encouraging users to use JIRI_ROOT/.jiri_root/scripts instead.
Also remove unused "run" and "must" functions.
Change-Id: I856498ac23872e863e13b5ba2ee8ee1e6f9bae73
diff --git a/public/bootstrap.sh b/public/bootstrap.sh
index e30c234..8eef3a6 100755
--- a/public/bootstrap.sh
+++ b/public/bootstrap.sh
@@ -20,27 +20,6 @@
done
}
-must() {
- "$@"
- if [[ "$?" -ne 0 ]]; then
- exit 1
- fi
-}
-
-run() {
- echo ">> $@"
- local OUTPUT
- OUTPUT=$("$@" 2>&1)
- if [[ "$?" -eq 0 ]]; then
- echo ">> OK"
- return 0
- else
- echo ">> FAILED"
- echo "${OUTPUT}"
- return 1
- fi
-}
-
check_environment() {
# Check that the JIRI_ROOT environment variable is set.
if [[ -z "${JIRI_ROOT}" ]]; then
@@ -130,9 +109,7 @@
retry $JIRI_ROOT/.jiri_root/bin/jiri update
popd
- echo "Recommended for contributors:"
- echo "Add ${JIRI_ROOT}/devtools/bin to your PATH."
-
+ echo "Recommended: Add ${JIRI_ROOT}/.jiri_root/scripts to your PATH."
trap - EXIT
}
