diff options
| author | Maxime Dénès | 2018-09-10 13:54:56 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-10 13:54:56 +0200 |
| commit | 2413031f6a5eeb0b49545a0b8ae312a99cbb5659 (patch) | |
| tree | 0cb372a509ac064a7c472285cdf8efb08cd6c7bb /.github | |
| parent | 2652465711423b0b332cfbb5f74145c48b53be1e (diff) | |
| parent | 9e7977e9c61ecbd64c1debaaefdd60ab2f362e5e (diff) | |
Merge PR #8430: 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 ########## |