diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 98fe2546b5..2a641263e3 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -37,6 +37,9 @@ *.nix @coq/nix-maintainers +azure-pipelines.yml @coq/ci-maintainers +/dev/ci/azure* @coq/ci-maintainers + ########## Documentation ########## /README.md @Zimmi48 @@ -68,6 +71,8 @@ /man/ @silene # Secondary maintainer @maximedenes +/doc/plugin_tutorial/ @ybertot + ########## Coqchk ########## /checker/ @ppedrot @@ -311,7 +316,7 @@ /test-suite/README.md @gares # Secondary maintainer @SkySkimmer -/test-suite/save-logs @SkySkimmer +/test-suite/report.sh @SkySkimmer /test-suite/complexity/ @herbelin |