diff --git a/ci/docker-run.sh b/ci/docker-run.sh index dc390fef65..507f9500ff 100755 --- a/ci/docker-run.sh +++ b/ci/docker-run.sh @@ -1,22 +1,30 @@ #!/bin/bash -e usage() { - echo "Usage: $0 [docker image name] [command]" + echo "Usage: $0 [--nopull] [docker image name] [command]" echo echo Runs command in the specified docker image with - echo a CI-appropriate environment + echo a CI-appropriate environment. + echo + echo "--nopull Skip the dockerhub image update" echo } cd "$(dirname "$0")/.." +NOPULL=false +if [[ $1 = --nopull ]]; then + NOPULL=true + shift +fi + IMAGE="$1" if [[ -z "$IMAGE" ]]; then echo Error: image not defined exit 1 fi -docker pull "$IMAGE" +$NOPULL || docker pull "$IMAGE" shift ARGS=(