aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github
diff options
context:
space:
mode:
authorGravatar Enrico <gares@fettunta.org>2018-03-20 18:05:37 +0000
committerGravatar GitHub <noreply@github.com>2018-03-20 18:05:37 +0000
commita56a31b31b25991dd867700840a8f23af3eeb454 (patch)
tree0277ea1bd4d854b08ab2e8907b3117fe20a60f8b /.github
parentbc0fa22b91b55a110def7daec66713d2a7fb909e (diff)
Update CODEOWNERS
Diffstat (limited to '.github')
-rw-r--r--.github/CODEOWNERS12
1 files changed, 9 insertions, 3 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 0f8b0a2cd..b64212dff 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -45,10 +45,15 @@
/plugins/btauto/ @ppedrot @herbelin
-/plugins/cc/ @herbelin # I don't know Pierre Corbineau's GitHub nickname
+# I don't know Pierre Corbineau's GitHub nickname
+/plugins/cc/ @herbelin
+
/plugins/derive/ @aspiwack @ppedrot
/plugins/extraction/ @letouzey @maximedenes
-/plugins/firstorder/ @herbelin # I don't know Pierre Corbineau's GitHub nickname
+
+ # I don't know Pierre Corbineau's GitHub nickname
+/plugins/firstorder/ @herbelin
+
/plugins/fourier/ @herbelin @gares
/plugins/funind/ @forestjulien @Matafou
/plugins/ltac/ @ppedrot
@@ -64,7 +69,8 @@
/plugins/quote/ @herbelin
-/plugins/rtauto/ @herbelin # Should be Pierre Corbineau too
+# Should be Pierre Corbineau too
+/plugins/rtauto/ @herbelin
/pretyping/ @mattam82 @gares
/printing/ @herbelin @mattam82