Go back to succeeding when the second make succeeds

JasonGross · Oct 18, 2022 · a477f10 · a477f10
1 parent 4a619d6
commit a477f10
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh
@@ -41,9 +41,10 @@ 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
+        make "$@" ${OUTPUT_SYNC} TIMED=1 TIMING=1 VERBOSE=1 || exit $?
+    else
+        exit 1
     fi
-    exit 1
 fi
 
 unameOut="$(uname -s)"