From 5900a4de58dbf54a7b31d23c3f2d123dc63ad82d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 26 Nov 2020 01:20:47 +0100 Subject: [PATCH] fix: Prepend 'exec 2>&1' to custom_script to untangle output * This patch workarounds GitHub Actions unflushed std(out/err) output. --- entrypoint.sh | 2 +- helper.sh | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/entrypoint.sh b/entrypoint.sh index fdb4cb3..8380b1c 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -141,7 +141,7 @@ echo "::add-matcher::$HOME/coq.json" docker run -i --init --rm --name=COQ -e WORKDIR="$WORKDIR" -e PACKAGE="$PACKAGE" \ -v "$HOST_WORKSPACE_REPO:$PWD" -w "$PWD" \ "$COQ_IMAGE" /bin/bash --login -c " -endGroup () { { init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endTime=\$(date -u +%s); echo \"::endgroup::\"; printf \"↳ \"; date -u -d \"@\$((endTime - startTime))\" '+%-Hh %-Mm %-Ss'; echo; unset startTime; else echo 'Error: missing startGroup command.'; case \"\$init_opts\" in *x*) set -x ;; esac; return 1; fi; case \"\$init_opts\" in *x*) set -x ;; esac; } ; startGroup () { { init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endGroup; fi; if [ \$# -ge 1 ]; then groupTitle=\"\$*\"; else groupTitle=\"Unnamed group\"; fi; echo; echo \"::group::\$groupTitle\"; startTime=\$(date -u +%s); case \"\$init_opts\" in *x*) set -x ;; esac; } # generated from helper.sh +exec 2>&1 ; endGroup () { { init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endTime=\$(date -u +%s); echo \"::endgroup::\"; printf \"↳ \"; date -u -d \"@\$((endTime - startTime))\" '+%-Hh %-Mm %-Ss'; echo; unset startTime; else echo 'Error: missing startGroup command.'; case \"\$init_opts\" in *x*) set -x ;; esac; return 1; fi; case \"\$init_opts\" in *x*) set -x ;; esac; } ; startGroup () { { init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endGroup; fi; if [ \$# -ge 1 ]; then groupTitle=\"\$*\"; else groupTitle=\"Unnamed group\"; fi; echo; echo \"::group::\$groupTitle\"; startTime=\$(date -u +%s); case \"\$init_opts\" in *x*) set -x ;; esac; } # generated from helper.sh export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '; set -ex $_OCAML407_COMMAND $INPUT_CUSTOM_SCRIPT" script diff --git a/helper.sh b/helper.sh index d8f905f..c4b92cf 100755 --- a/helper.sh +++ b/helper.sh @@ -45,6 +45,7 @@ main_helper () { set -x exec > "$gen_file" + echo -n 'exec 2>&1 ; ' # workaround GHA unflushed stdout/stderr minimify endGroup echo -n ' ; ' minimify startGroup