From d8188759091e64f92c0dcb2b458dd8c23a590be4 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 14 Aug 2018 09:40:48 +0200
Subject: Introduce a team of code owners for the documentation.

As was previously done for the CI, this means that there are no more
principal / secondary code owners. All the member of the team can
choose to review and self-assign any documentation PR that is not
their own.
---
 .github/CODEOWNERS | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 20d49e675f..5be434c8b7 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -42,11 +42,7 @@
 # Trick to avoid getting review requests
 # each time someone modifies the dev changelog
 
-/doc/             @maximedenes
-# Secondary maintainer @silene @Zimmi48
-
-/doc/tools/coqrst/ @maximedenes
-# Secondary maintainer @cpitclaudel
+/doc/             @coq/doc-maintainers
 
 /man/             @silene
 # Secondary maintainer @maximedenes
-- 
cgit v1.2.3