diff options
| author | Maxime Dénès | 2018-03-29 13:14:27 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-29 13:14:27 +0200 |
| commit | 9fa5f99783848eff9e94887562464efe7d1e3fe8 (patch) | |
| tree | 8ecda605480806688ef06ec9569bd7ad480b7bb0 | |
| parent | bd8606189268c3fcdd3506872d459cb9032a33bf (diff) | |
| parent | b0f2d435bbb0b78f164876b765c8c97c6be2eecd (diff) | |
Merge PR #7072: Update codeowners
| -rw-r--r-- | .github/CODEOWNERS | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index fea50c58cd..f344c5cf55 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -37,6 +37,10 @@ /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes +/dev/doc/changes.md @ghost +# Trick to avoid getting review requests +# each time someone modifies the dev changelog + /doc/ @maximedenes # Secondary maintainer @silene @@ -104,8 +108,8 @@ /plugins/btauto/ @ppedrot # Secondary maintainer @herbelin -# I don't know Pierre Corbineau's GitHub nickname -/plugins/cc/ @herbelin +/plugins/cc/ @PierreCorbineau +# Secondary maintainer @herbelin /plugins/derive/ @aspiwack # Secondary maintainer @ppedrot @@ -113,8 +117,8 @@ /plugins/extraction/ @letouzey # Secondary maintainer @maximedenes -# I don't know Pierre Corbineau's GitHub nickname -/plugins/firstorder/ @herbelin +/plugins/firstorder/ @PierreCorbineau +# Secondary maintainer @herbelin /plugins/fourier/ @herbelin # Secondary maintainer @gares @@ -149,8 +153,8 @@ /plugins/quote/ @herbelin -# Should be Pierre Corbineau too -/plugins/rtauto/ @herbelin +/plugins/rtauto/ @PierreCorbineau +# Secondary maintainer @herbelin ########## Pretyper ########## @@ -294,6 +298,9 @@ /META.coq @ejgallego # Secondary maintainer @letouzey +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## Developer tools ########## |