Remove --output-sync from build log when make fails (mit-plv#2010)

This should make it a bit easier to debug cases like mit-plv#2009 (comment)
JasonGross · Jan 31, 2025 · f47be1a · f47be1a
1 parent dd6d684
commit f47be1a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh
@@ -61,7 +61,7 @@ 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 $?
+        make "$@" TIMED=1 TIMING=1 VERBOSE=1 || exit $?
     else
         exit 1
     fi