}
docker_push () {
- docker push $*
-
- ECODE=$?
+ # Sometimes docker push fails; retry it a few times if necessary.
+ for i in `seq 1 5`; do
+ $DOCKER push $*
+ ECODE=$?
+ if [[ "$ECODE" == "0" ]]; then
+ break
+ fi
+ done
if [[ "$ECODE" != "0" ]]; then
title "!!!!!! docker push $* failed !!!!!!"
fi
}
+# Sanity check
+if ! [[ -n "$WORKSPACE" ]]; then
+ echo >&2
+ echo >&2 "Error: WORKSPACE environment variable not set"
+ echo >&2
+ exit 1
+fi
+
echo $WORKSPACE
+# find the docker binary
+DOCKER=`which docker.io`
+
+if [[ "$DOCKER" == "" ]]; then
+ DOCKER=`which docker`
+fi
+
+if [[ "$DOCKER" == "" ]]; then
+ title "Error: you need to have docker installed. Could not find the docker executable."
+ exit 1
+fi
+
# DOCKER
title "Starting docker build"