Skip to content

Commit

Permalink
Revert "Go back to succeeding when the second make succeeds"
Browse files Browse the repository at this point in the history
This reverts commit a477f10.
  • Loading branch information
JasonGross committed Nov 7, 2022
1 parent b6dae11 commit 2323a2b
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions etc/ci/github-actions-make.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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)"
Expand Down

0 comments on commit 2323a2b

Please sign in to comment.