From 1790f4336dd0cd6a8ac4c013d4dc4d3463aaa47e Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 28 Jun 2018 11:03:37 +0200
Subject: Update maintainers for native/VM files in pretyping

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

(limited to '.github')

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 3a762b42a..eb2797101 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -186,6 +186,10 @@
 /pretyping/       @mattam82
 # Secondary maintainer @gares
 
+/pretyping/vnorm.*     @maximedenes
+/pretyping/nativenorm.* @maximedenes
+# Secondary maintainer @ppedrot
+
 ########## Pretty printer ##########
 
 /printing/        @herbelin
-- 
cgit v1.2.3