Revert "Go back to succeeding when the second make succeeds"

This reverts commit a477f10.
mit-plv · Oct 18, 2022 · 120d6cb · 120d6cb
1 parent 46ec5b2
commit 120d6cb
Showing 1 changed file with 2 additions and 3 deletions.
diff --git 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)"