diff options
Diffstat (limited to '.github/CODEOWNERS')
| -rw-r--r-- | .github/CODEOWNERS | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2ca827492..eeeb17b61 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -59,7 +59,7 @@ ########## Coqchk ########## /checker/ @barras -# Secondary maintainer @maximedenes +# Secondary maintainers @maximedenes @ppedrot ########## Coq lib ########## @@ -100,7 +100,7 @@ ########## Kernel ########## /kernel/ @maximedenes -# Secondary maintainer @barras +# Secondary maintainers @barras @ppedrot /kernel/byterun/ @maximedenes # Secondary maintainer @silene |