diff options
Diffstat (limited to '.gitlab')
| -rwxr-xr-x | .gitlab/ci.sh | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh index c1e666e540..66c52a7c94 100755 --- a/.gitlab/ci.sh +++ b/.gitlab/ci.sh @@ -574,6 +574,14 @@ if [ "${CI_MERGE_REQUEST_SOURCE_BRANCH_NAME:-}" == "wip/marge_bot_batch_merge_jo echo "Ignoring perf failures" fi fi +echo "CI_COMMIT_BRANCH: $CI_COMMIT_BRANCH" +echo "CI_PROJECT_PATH: $CI_PROJECT_PATH" +if [ "${CI_COMMIT_BRANCH:-}" == "master" ] && [ "${CI_PROJECT_PATH:-}" == "ghc/ghc" ]; then + if [ -z "${IGNORE_PERF_FAILURES:-}" ]; then + IGNORE_PERF_FAILURES="decreases" + echo "Ignoring perf failures" + fi +fi if [ -n "${IGNORE_PERF_FAILURES:-}" ]; then RUNTEST_ARGS="--ignore-perf-failures=$IGNORE_PERF_FAILURES" fi |