diff options
| author | Gaëtan Gilbert | 2018-12-12 14:10:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-17 16:42:36 +0100 |
| commit | bb1c89a486d47dbf497756b8374337a6857a96de (patch) | |
| tree | 82e30800cd9c23a903b5cd6d528d1b8243e4a98f /.github/CODEOWNERS | |
| parent | 9349e0367d2d50b11ccd31c8f6d1979ebd52e555 (diff) | |
Set up CI with Azure Pipelines
Diffstat (limited to '.github/CODEOWNERS')
| -rw-r--r-- | .github/CODEOWNERS | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 98fe2546b5..0f2dd89975 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 |