From a56a31b31b25991dd867700840a8f23af3eeb454 Mon Sep 17 00:00:00 2001 From: Enrico Date: Tue, 20 Mar 2018 18:05:37 +0000 Subject: Update CODEOWNERS --- .github/CODEOWNERS | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to '.github') 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 -- cgit v1.2.3