aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-29 11:09:35 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-29 11:09:35 +0200
commitb0f2d435bbb0b78f164876b765c8c97c6be2eecd (patch)
treed50e16918516cfc486986328c6a26e0210ca7a4e /.github
parent092c35f88566e11562a1c10e22e551c2d635439b (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/CODEOWNERS4
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