diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-20 19:08:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-20 19:08:46 +0100 |
| commit | 17c94dca5fe2fc19137b9cac923d51e8eb818041 (patch) | |
| tree | 0277ea1bd4d854b08ab2e8907b3117fe20a60f8b /.github | |
| parent | bc0fa22b91b55a110def7daec66713d2a7fb909e (diff) | |
| parent | a56a31b31b25991dd867700840a8f23af3eeb454 (diff) | |
Merge PR #7022: Update CODEOWNERS
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 12 |
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 |