diff options
| author | Théo Zimmermann | 2019-01-23 09:29:13 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-23 09:29:13 +0100 |
| commit | c845fed94ab68f7891e08d0a8aabc1a7ddff11eb (patch) | |
| tree | a2e96b16c8d3b669d37969008a9b32d0f2347928 /.github | |
| parent | 9e7f3ab6bee7543fbd2929e5c909a65c4d46a6bf (diff) | |
| parent | 9f58e0a4fa814484f188236ebb39e86dd737d218 (diff) | |
Merge PR #9382: Transfer maintenance of appveyor infrastructure to the CI team
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
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 |