diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 324889ec90..512a9c99eb 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -24,6 +24,7 @@ /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers /Makefile.ci @coq/ci-maintainers +/dev/ci/nix @coq/nix-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests |