From d8603ba5bc093a479bc30df580f4f25709681c16 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 26 Mar 2018 10:39:05 +0200
Subject: Use Pierre Corbineau GitHub nickname in CODEOWNERS.

---
 .github/CODEOWNERS | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index fea50c58cd..ee291aebbe 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -104,8 +104,8 @@
 /plugins/btauto/  @ppedrot
 # Secondary maintainer @herbelin
 
-# I don't know Pierre Corbineau's GitHub nickname
-/plugins/cc/            @herbelin
+/plugins/cc/           @PierreCorbineau
+# Secondary maintainer @herbelin
 
 /plugins/derive/        @aspiwack
 # Secondary maintainer @ppedrot
@@ -113,8 +113,8 @@
 /plugins/extraction/    @letouzey
 # Secondary maintainer @maximedenes
 
-# I don't know Pierre Corbineau's GitHub nickname
-/plugins/firstorder/    @herbelin
+/plugins/firstorder/   @PierreCorbineau
+# Secondary maintainer @herbelin
 
 /plugins/fourier/       @herbelin
 # Secondary maintainer @gares
@@ -149,8 +149,8 @@
 
 /plugins/quote/ @herbelin
 
-# Should be Pierre Corbineau too
-/plugins/rtauto/ @herbelin
+/plugins/rtauto/       @PierreCorbineau
+# Secondary maintainer @herbelin
 
 ########## Pretyper ##########
 
-- 
cgit v1.2.3


From 092c35f88566e11562a1c10e22e551c2d635439b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 26 Mar 2018 10:41:02 +0200
Subject: Add Michael Soegtrop as a code owner for Windows build scripts.

---
 .github/CODEOWNERS | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index ee291aebbe..d33a0c59fd 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -294,6 +294,9 @@
 /META.coq         @ejgallego
 # Secondary maintainer @letouzey
 
+/dev/build/windows @MSoegtropIMC
+# Secondary maintainer @maximedenes
+
 
 ########## Developer tools ##########
 
-- 
cgit v1.2.3


From b0f2d435bbb0b78f164876b765c8c97c6be2eecd Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 29 Mar 2018 11:09:35 +0200
Subject: 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.
---
 .github/CODEOWNERS | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index d33a0c59fd..f344c5cf55 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
 
-- 
cgit v1.2.3