diff options
Diffstat (limited to '.github/CODEOWNERS')
| -rw-r--r-- | .github/CODEOWNERS | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 56f48aaa4f..9e2af04e28 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -14,7 +14,7 @@ /configure* @coq/legacy-build-maintainers @coq/build-maintainers -/META.coq.in @coq/legacy-build-maintainers +/META.coq-core.in @coq/legacy-build-maintainers ########## CI infrastructure ########## |