diff options
| author | Théo Zimmermann | 2018-11-22 13:56:24 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-11-22 13:57:49 +0100 |
| commit | cca54c53b4324e0b4630ba9da2d48a117252cece (patch) | |
| tree | 8d2ae22683aa2baa5c8bd8042f0aeaa106d8d2d9 /.github | |
| parent | 29adf6d7d040a1721e63e1ad02bb1c3e8847ff8c (diff) | |
New code owner team ssreflect-maintainers.
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 802c1da221..511c2b47d8 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -166,12 +166,9 @@ /plugins/setoid_ring/ @amahboubi # Secondary maintainer @bgregoir -/plugins/ssrmatching/ @gares -# Secondary maintainer @maximedenes - -/plugins/ssr/ @gares -/test-suite/ssr/ @gares -# Secondary maintainer @maximedenes +/plugins/ssrmatching/ @coq/ssreflect-maintainers +/plugins/ssr/ @coq/ssreflect-maintainers +/test-suite/ssr/ @coq/ssreflect-maintainers /plugins/syntax/ @ppedrot # Secondary maintainer @maximedenes |