aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-18 14:41:59 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-20 16:10:12 +0200
commit28f7d26cc21013027d6a73701d19a7d532695470 (patch)
treede3c42d6afb733528f9f94e5e33abce9a5e94b47 /.github
parentd6eb4a26648817f6b034e95c02622cadf0fa65ca (diff)
Make Pierre-Marie a secondary maintainer of the kernel and checker.
[ci skip]
Diffstat (limited to '.github')
-rw-r--r--.github/CODEOWNERS4
1 files changed, 2 insertions, 2 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 2ca827492..eeeb17b61 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -59,7 +59,7 @@
########## Coqchk ##########
/checker/ @barras
-# Secondary maintainer @maximedenes
+# Secondary maintainers @maximedenes @ppedrot
########## Coq lib ##########
@@ -100,7 +100,7 @@
########## Kernel ##########
/kernel/ @maximedenes
-# Secondary maintainer @barras
+# Secondary maintainers @barras @ppedrot
/kernel/byterun/ @maximedenes
# Secondary maintainer @silene