From 7bf7d431eaf1fe5d522ae41028f065d5c33b866d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 18 Oct 2018 17:53:50 +0200
Subject: Give code ownership of merging doc to pushers team to notify members
 when it changes.

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

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 412bed8334..324889ec90 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -53,6 +53,10 @@
 /dev/doc/         @Zimmi48
 # Secondary maintainer @maximedenes
 
+/dev/doc/MERGING.md @coq/pushers
+# This ensures that all members of the @coq/pushers
+# team are notified when the merging doc changes.
+
 /dev/doc/changes.md    @ghost
 # Trick to avoid getting review requests
 # each time someone modifies the dev changelog
-- 
cgit v1.2.3