diff options
| author | Théo Zimmermann | 2018-08-25 17:28:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-05 11:44:07 +0200 |
| commit | a325b3026c2569f3c60364509d9b08925c16c6dc (patch) | |
| tree | a6f7173a391d82fa7e32d29c2d48f3fa32b74340 | |
| parent | 6d14f27dc75c68d9964755540ae795332eac3844 (diff) | |
Owners of Makefile.{ci,doc} are teams {ci,doc}-maintainers.
| -rw-r--r-- | .github/CODEOWNERS | 32 |
1 files changed, 13 insertions, 19 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 5be434c8b7..c844fd7136 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 @@ -43,6 +55,7 @@ # each time someone modifies the dev changelog /doc/ @coq/doc-maintainers +/Makefile.doc @coq/doc-maintainers /man/ @silene # Secondary maintainer @maximedenes @@ -292,25 +305,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 |