From 9400bb481a770209f52ebd0b6f6ce960970d5084 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 18 Oct 2022 09:28:52 -0400
Subject: [PATCH] Revert "Go back to succeeding when the second make succeeds"

This reverts commit a477f10331b7bbb20a8e446edbd137e067bebe0f.
---
 etc/ci/github-actions-make.sh | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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)"