From ecddff98f5a34ff91d68d949d0bcd543120569ae Mon Sep 17 00:00:00 2001
From: Michael Vines <mvines@gmail.com>
Date: Mon, 20 Aug 2018 10:17:12 -0700
Subject: [PATCH] Add --nopull argument

---
 ci/docker-run.sh | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

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=(