about summary refs log tree commit diff homepage
path: root/scripts
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-03-14 15:50:39 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-03-17 15:43:21 +0000
commit2b78b22ae5f74d32b6e0da086af37389cf9761c8 (patch)
tree1335aa23b2b8a6e925f0be62432be75f18285a21 /scripts
parentf7612f0cfd68a157a5998649d070ef03e62fb89e (diff)
downloadklee-2b78b22ae5f74d32b6e0da086af37389cf9761c8.tar.gz
Fix `true` invocation in case docker image could not be pushed
Diffstat (limited to 'scripts')
-rwxr-xr-xscripts/build/build.sh2
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