diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2a641263e3..275d6c1ff5 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -30,10 +30,9 @@ # Trick to avoid getting review requests # each time someone adds an overlay -/appveyor.yml @maximedenes -/dev/ci/appveyor.* @maximedenes -/dev/ci/*.bat @maximedenes -# Secondary maintainer @SkySkimmer +/appveyor.yml @coq/ci-maintainers +/dev/ci/appveyor.* @coq/ci-maintainers +/dev/ci/*.bat @coq/ci-maintainers *.nix @coq/nix-maintainers @@ -71,7 +70,7 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes -/doc/plugin_tutorial/ @ybertot +/doc/plugin_tutorial/ @coq/plugin-tutorial-maintainers ########## Coqchk ########## |