diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 54d9ccaf19..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 |