diff options
Diffstat (limited to 'ci/run-docker.sh')
| -rwxr-xr-x | ci/run-docker.sh | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/ci/run-docker.sh b/ci/run-docker.sh index 4247827f67..1e65795ebf 100755 --- a/ci/run-docker.sh +++ b/ci/run-docker.sh @@ -7,6 +7,14 @@ set -ex run() { echo "Building docker container for target ${1}" + + # FIXME: Hacky workaround. Docker build seems to work better if we pull the base images first + ubuntu_images=( 16.04 17.10 18.04 ) + for i in "${ubuntu_images[@]}" + do + docker pull ubuntu:$i + done + # use -f so we can use ci/ as build context docker build -t libc -f "ci/docker/${1}/Dockerfile" ci/ mkdir -p target |