diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh index 27419804e7e..e18ce4f08ca 100755 --- a/etc/ci/github-actions-make.sh +++ b/etc/ci/github-actions-make.sh @@ -43,10 +43,9 @@ cat time-of-build-pretty.log if [ ! -f finished.ok ]; then # see https://stackoverflow.com/a/15394738/377022 for more alternatives if [[ ! " $* " =~ " validate " ]]; then - make "$@" ${OUTPUT_SYNC} TIMED=1 TIMING=1 VERBOSE=1 || exit $? - else - exit 1 + make "$@" ${OUTPUT_SYNC} TIMED=1 TIMING=1 VERBOSE=1 fi + exit 1 fi unameOut="$(uname -s)"