diff options
| -rw-r--r-- | .github/CODEOWNERS | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2a325f2d71..698452cb2b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -1,10 +1,17 @@ # This file describes the maintainers for the main components. See # `dev/doc/MERGING.md`. -########## GitHub metadata, including this file ########## +########## Contributing process ########## -/.github/ @maximedenes -# Secondary maintainer @Zimmi48 +/.github/ @coq/contributing-process-maintainers + +/CONTRIBUTING.md @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 ########## @@ -45,19 +52,12 @@ azure-pipelines.yml @coq/ci-maintainers /INSTALL* @Zimmi48 # Secondary maintainer @maximedenes -/CONTRIBUTING.md @Zimmi48 -# Secondary maintainer @maximedenes - /CODE_OF_CONDUCT.md @Zimmi48 # Secondary maintainer @mattam82 /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes -/dev/doc/MERGING.md @coq/pushers -# This ensures that all members of the @coq/pushers -# team are notified when the merging doc changes. - /dev/doc/changes.md @ghost # Trick to avoid getting review requests # each time someone modifies the dev changelog |