diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-29 11:09:35 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-29 11:09:35 +0200 |
commit | b0f2d435bbb0b78f164876b765c8c97c6be2eecd (patch) | |
tree | d50e16918516cfc486986328c6a26e0210ca7a4e /.github | |
parent | 092c35f88566e11562a1c10e22e551c2d635439b (diff) |
Remove dev/doc/changes.md from files with a code owner.
Like CHANGES, and the test-suite folder, this file receives too many
updates to have a code owner. It is the job of the reviewer of the PR
to review changes to these files as well.
Diffstat (limited to '.github')
-rw-r--r-- | .github/CODEOWNERS | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index d33a0c59f..f344c5cf5 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -37,6 +37,10 @@ /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes +/dev/doc/changes.md @ghost +# Trick to avoid getting review requests +# each time someone modifies the dev changelog + /doc/ @maximedenes # Secondary maintainer @silene |