diff options
| author | Théo Zimmermann | 2018-09-07 11:43:50 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-07 11:43:50 +0200 |
| commit | 9e7977e9c61ecbd64c1debaaefdd60ab2f362e5e (patch) | |
| tree | 9d44830bcc0f88bf45dc2125938826ae916498dc /.github | |
| parent | 07c3905c30590c93f1b173833087bbd1df364227 (diff) | |
Move to a team of code owners for the Nix files.
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 274a0001b1..2d2a61cb9e 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -21,8 +21,7 @@ /dev/ci/*.bat @maximedenes # Secondary maintainer @SkySkimmer -/default.nix @Zimmi48 -# Secondary maintainer @vbgl +*.nix @coq/nix-maintainers ########## Documentation ########## |