diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-07-16 13:27:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-07-16 13:27:08 +0200 |
| commit | e27d2fd32e40937e48889772361f1cf53dd9c48e (patch) | |
| tree | 5a5e6aaf009fa5ab5ee1b376ba38dbaa76a2f392 | |
| parent | ad5d90e30d52038c22a5315cbf84aa30aa021875 (diff) | |
| parent | 55f59acbd9cdec6188613edc29e49d5f5a4f6d98 (diff) | |
Merge PR #8023: Introduce a team of code owners for the CI system.
| -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 |