diff options
| -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 ########## |