diff options
author | Tom Parker-Shemilt <palfrey@tevp.net> | 2018-11-24 19:18:51 +0000 |
---|---|---|
committer | Tom Parker-Shemilt <palfrey@tevp.net> | 2018-11-24 19:18:51 +0000 |
commit | b05e05819da2e2cc3dc15deb6c784bdee3328f3f (patch) | |
tree | cd2568f40875fe08a7a209abd35770ab165df145 /ci/run-docker.sh | |
parent | 75071fe11f9b44130d273fb4d91e001ea04f2551 (diff) | |
download | rust-libc-b05e05819da2e2cc3dc15deb6c784bdee3328f3f.tar.gz |
Download Docker images first as that seems to work better at least locally
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 |