diff options
| author | Vincent Laporte | 2018-11-12 16:09:48 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-11-12 16:10:20 +0000 |
| commit | 274411f257e84d6552c3da163dd5420cd46db841 (patch) | |
| tree | c520be8f2f08996d3f90a5357df490c1a849c718 /.github | |
| parent | 7e014333c57bdede663e490743bc84f696764381 (diff) | |
Set codeowners for dev/ci/nix
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 |