diff options
| author | Moritz Angermann <moritz.angermann@gmail.com> | 2021-03-16 17:53:43 +0800 |
|---|---|---|
| committer | Moritz Angermann <moritz.angermann@gmail.com> | 2021-03-29 09:43:22 +0800 |
| commit | 07b859592fa0e804ecaf6c8432bb1e2d2242e1f1 (patch) | |
| tree | fe4a109aa7f58c2697bc1c610ed9c06b8a73ce23 | |
| parent | 3f3b8362cdb80d5d7fa0a697aa4eb7e019f584fc (diff) | |
| download | haskell-07b859592fa0e804ecaf6c8432bb1e2d2242e1f1.tar.gz | |
[ci] don't make marge double build.
This fixes !18744
| -rw-r--r-- | .gitlab-ci.yml | 32 |
1 files changed, 24 insertions, 8 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 774f5dc650..c863323fcd 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -47,14 +47,30 @@ stages: - testing # head.hackage correctness and compiler performance testing - deploy # push documentation -# N.B.Don't run on wip/ branches, instead on run on merge requests. -.only-default: &only-default - only: - - master - - /ghc-[0-9]+\.[0-9]+/ - - merge_requests - - tags - - web +# Note [The CI Story] +# ~~~~~~~~~~~~~~~~~~~ +# +# There are two different types of pipelines: +# +# - marge-bot merges to `master`. Here we perform an exhaustive validation +# across all of the platforms which we support. In addition, we push +# performance metric notes upstream, providing a persistent record of the +# performance characteristics of the compiler. +# +# - merge requests. Here we perform a slightly less exhaustive battery of +# testing. Namely we omit some configurations (e.g. the unregisterised job). +# These use the merge request's base commit for performance metric +# comparisons. +# + +workflow: + # N.B. Don't run on wip/ branches, instead on run on merge requests. + rules: + - if: $CI_MERGE_REQUEST_ID + - if: $CI_COMMIT_TAG + - if: '$CI_COMMIT_BRANCH == "master"' + - if: '$CI_COMMIT_BRANCH =~ /ghc-[0-9]+\.[0-9]+/' + - if: '$CI_PIPELINE_SOURCE == "web"' .nightly: &nightly only: |