diff options
| -rw-r--r-- | jenkins-common.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/jenkins-common.sh b/jenkins-common.sh index 88d053c..3511c02 100644 --- a/jenkins-common.sh +++ b/jenkins-common.sh @@ -121,10 +121,12 @@ docker_images_require() { for i in $@; do # Don't build images that are available on the private - # registry, if using it. + # registry, if using it. Instead, pull the images to make sure + # they are up-to-date. if [ "$REGISTRY_HOST" = "registry.osmocom.org" ]; then case "$i" in debian-stretch-titan) + docker pull "$REGISTRY_HOST/$USER/$i" continue ;; esac |