diff options
| author | Maxime Dénès | 2019-01-22 23:24:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-22 23:24:09 +0100 |
| commit | 9f58e0a4fa814484f188236ebb39e86dd737d218 (patch) | |
| tree | 039f6483c10c21c06943710f42d53bca3e3a5a04 /.github | |
| parent | 03c17218eeacb098ff57ecee1d98f46b7c8fa185 (diff) | |
Transfer maintenance of appveyor infrastructure to the CI team
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 2a641263e3..ecfeac65ad 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 |