diff options
| author | coqbot-app[bot] | 2021-04-07 17:44:22 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-07 17:44:22 +0000 |
| commit | 59d0462f35818c12a0727a560d7b9ecf2ceea994 (patch) | |
| tree | 5b01de7e969b000fa64cc7edca60323eb11958d7 /dev/ci | |
| parent | d98faea005d32b64252bf6bd50eb01f320a2bc8c (diff) | |
| parent | 7769a1f12baa19ef1d0bccb4db36168f0fe0dcc1 (diff) | |
Merge PR #14032: CI: don't output-sync
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-common.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 006565df5c..6d1e6d788a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -138,8 +138,8 @@ make() if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; then # Not submake and parallel make requested - command make --output-sync -j "$NJOBS" "$@" + command make -j "$NJOBS" "$@" else - command make --output-sync "$@" + command make "$@" fi } |