From f47be1a6a50bd1f564070a14da8302ab6eccb05e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Jan 2025 12:53:24 -0800 Subject: [PATCH] Remove --output-sync from build log when make fails (#2010) This should make it a bit easier to debug cases like https://github.com/mit-plv/fiat-crypto/pull/2009#issuecomment-2627878238 --- etc/ci/github-actions-make.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh index 210872b92d..52def75b1f 100755 --- 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