diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-03-14 15:50:39 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-17 15:43:21 +0000 |
| commit | 2b78b22ae5f74d32b6e0da086af37389cf9761c8 (patch) | |
| tree | 1335aa23b2b8a6e925f0be62432be75f18285a21 /scripts/build | |
| parent | f7612f0cfd68a157a5998649d070ef03e62fb89e (diff) | |
| download | klee-2b78b22ae5f74d32b6e0da086af37389cf9761c8.tar.gz | |
Fix `true` invocation in case docker image could not be pushed
Diffstat (limited to 'scripts/build')
| -rwxr-xr-x | scripts/build/build.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/build/build.sh b/scripts/build/build.sh index feda6bfe..ebbcde1a 100755 --- a/scripts/build/build.sh +++ b/scripts/build/build.sh @@ -337,7 +337,7 @@ build_docker() { # Build Docker container docker build -t "${REPOSITORY}/${target_image}" -f "${temp_dir}"/Dockerfile "${docker_context}" || return 1 if [[ "${PUSH_DOCKER_DEPS}" -eq 1 && "${is_dependency}" -eq 1 ]]; then - docker push "${REPOSITORY}/${target_image}" || /usr/bin/true + docker push "${REPOSITORY}/${target_image}" || true fi if [[ "${KEEP_DOCKERFILE}" -eq 0 ]]; then |