From 8fd24bc02e5ed03593ee665d9a52903f97b8eac5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 24 Dec 2019 19:55:32 +0100
Subject: Update merging doc following the full move to teams.

Integrate merging doc in the main contributing document.
---
 .github/CODEOWNERS | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to '.github')

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 2f90895279..a7c0846e35 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -6,13 +6,10 @@
 /.github/                   @coq/contributing-process-maintainers
 
 /CONTRIBUTING.md            @coq/contributing-process-maintainers
+/dev/doc/shield-icon.png    @coq/contributing-process-maintainers
 
 /dev/doc/release-process.md @coq/contributing-process-maintainers
 
-/dev/doc/MERGING.md         @coq/pushers
-# This ensures that all members of the @coq/pushers
-# team are notified when the merging doc changes.
-
 ########## Build system ##########
 
 /Makefile*                      @coq/legacy-build-maintainers
-- 
cgit v1.2.3