diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2f90895279..a7c0846e35 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,13 +6,10 @@ /.github/ @coq/contributing-process-maintainers /CONTRIBUTING.md @coq/contributing-process-maintainers +/dev/doc/shield-icon.png @coq/contributing-process-maintainers /dev/doc/release-process.md @coq/contributing-process-maintainers -/dev/doc/MERGING.md @coq/pushers -# This ensures that all members of the @coq/pushers -# team are notified when the merging doc changes. - ########## Build system ########## /Makefile* @coq/legacy-build-maintainers |