From 1b2d2bdaa44798377fb2e853278013621140e6d5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 25 Aug 2020 09:06:45 +0200
Subject: Add /dev/bench to CODEOWNERS

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

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index c4d202470d..bb0beb142a 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -34,6 +34,8 @@
 # Trick to avoid getting review requests
 # each time someone adds an overlay
 
+/dev/bench/            @coq/bench-maintainers
+
 ########## Documentation ##########
 
 /README.md             @coq/doc-maintainers
-- 
cgit v1.2.3