Use curl instead of wget
It has fewer dependencies and tends to be installed by default in more
places.
Change-Id: Ieb7809875e029cda02b6ab25ac74c9a7ac0f4633
diff --git a/tools/bazel b/tools/bazel
index d305cf5..d9b6c86 100755
--- a/tools/bazel
+++ b/tools/bazel
@@ -60,11 +60,12 @@
# Now, download into the ~/.cache folder
if [ ! -e "${HOME}/.cache/bazel/${INSTALLER_NAME}" ];
then
+ NOISINESS=--silent
if [ -t 0 ] ; then
- wget "${DOWNLOAD_URL}" -O "${INSTALLER_NAME}" --no-verbose --show-progress
- else
- wget "${DOWNLOAD_URL}" -O "${INSTALLER_NAME}" --no-verbose --quiet
+ echo on terminal
+ NOISINESS=
fi
+ curl --output "${INSTALLER_NAME}" "${DOWNLOAD_URL}" ${NOISINESS}
mv "${INSTALLER_NAME}" "${HOME}/.cache/bazel/${INSTALLER_NAME}"
fi
rm -rf "${DOWNLOAD_TEMP_DIR}"