diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-09 13:11:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-09 13:11:49 +0200 |
| commit | 55f59acbd9cdec6188613edc29e49d5f5a4f6d98 (patch) | |
| tree | 3ef86ecf1f9300fbf7e7260a2a51e868a78cf2ce | |
| parent | a44b4be1bf8b96e941216cd10cfb5981a825c3fa (diff) | |
Introduce a team of code owners for the CI system.
This means that all the members of the team will receive
a review request for PRs on the CI, but only one of them
will need to approve the PR, and this will remove the
review request for the others.
Currently the team contains Emilio and Gaetan, the two
former code owners of these files. It makes sense to start
experimenting on this component since they had already
decided to make their role symmetric.
Updating the list of maintainers can be done by updating
the list members, and without changing the CODEOWNER file.
| -rw-r--r-- | .github/CODEOWNERS | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 192a2b181..bbd2d349c 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -8,22 +8,15 @@ ########## CI infrastructure ########## -/dev/ci/ @ejgallego -# Secondary maintainer @SkySkimmer +/dev/ci/ @coq/ci-maintainers +/.circleci/ @coq/ci-maintainers +/.travis.yml @coq/ci-maintainers +/.gitlab-ci.yml @coq/ci-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests # each time someone adds an overlay -/.circleci/ @SkySkimmer -# Secondary maintainer @ejgallego - -/.travis.yml @ejgallego -# Secondary maintainer @SkySkimmer - -/.gitlab-ci.yml @SkySkimmer -# Secondary maintainer @ejgallego - /appveyor.yml @maximedenes /dev/ci/appveyor.* @maximedenes /dev/ci/*.bat @maximedenes |