diff options
| author | Maxime Dénès | 2018-09-10 15:07:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-10 15:07:42 +0200 |
| commit | 90a0357108769355025e8f15a6fbf6766aed8d44 (patch) | |
| tree | e72decfdd385c649334d422f5b5ec6cf6b02220f /.github | |
| parent | 2413031f6a5eeb0b49545a0b8ae312a99cbb5659 (diff) | |
| parent | a325b3026c2569f3c60364509d9b08925c16c6dc (diff) | |
Merge PR #8323: Owners of Makefile.{ci,doc} are teams {ci,doc}-maintainers.
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 32 |
1 files changed, 13 insertions, 19 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2d2a61cb9e..d9136ee24b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,11 +6,23 @@ /.github/ @maximedenes # Secondary maintainer @Zimmi48 +########## Build system ########## + +/Makefile* @gares + +/configure* @ejgallego + +/META.coq.in @ejgallego + +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## CI infrastructure ########## /dev/ci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers +/Makefile.ci @coq/ci-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests @@ -42,6 +54,7 @@ # each time someone modifies the dev changelog /doc/ @coq/doc-maintainers +/Makefile.doc @coq/doc-maintainers /man/ @silene # Secondary maintainer @maximedenes @@ -301,25 +314,6 @@ /vernac/ @mattam82 # Secondary maintainer @maximedenes -########## Build system ########## - -/Makefile* @gares - -/configure* @ejgallego - -/META.coq.in @ejgallego - -/dev/build/windows @MSoegtropIMC -# Secondary maintainer @maximedenes - -# This file belongs to CI -/Makefile.ci @ejgallego -# Secondary maintainer @SkySkimmer - -# This file belongs to the doc -/Makefile.doc @maximedenes -# Secondary maintainer @silene - ########## Test suite ########## /test-suite/Makefile @gares |