aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-25 15:27:02 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-25 15:33:25 +0200
commit315cc7ad85b96dd5155f8ec0516b43af64e62a8b (patch)
treea0db0148c363f9b09fe3cd7e57cb036e4e3cfd6f /.github
parent89bfc37b26d79f5e29c079fee912bb2bfaa9b07c (diff)
Change primary maintainer for the checker.
Primary maintainers should be responsive. [ci skip]
Diffstat (limited to '.github')
-rw-r--r--.github/CODEOWNERS6
1 files changed, 3 insertions, 3 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 119ce082d..782efb5be 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -58,9 +58,9 @@
########## Coqchk ##########
-/checker/ @barras
-/test-suite/coqchk/ @barras
-# Secondary maintainers @maximedenes @ppedrot
+/checker/ @ppedrot
+/test-suite/coqchk/ @ppedrot
+# Secondary maintainers @maximedenes
########## Coq lib ##########