diff options
| author | Théo Zimmermann | 2019-12-24 19:55:32 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-24 20:07:49 +0100 |
| commit | 8fd24bc02e5ed03593ee665d9a52903f97b8eac5 (patch) | |
| tree | 61a66efcb99dbcfb67962639344e7e5ce2be2e81 /.github | |
| parent | c32e1c54c87231b6411d3002766972e18438fc4a (diff) | |
Update merging doc following the full move to teams.
Integrate merging doc in the main contributing document.
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 |