diff options
Diffstat (limited to '.github/CODEOWNERS')
| -rw-r--r-- | .github/CODEOWNERS | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index f802040a1d..06a733be45 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -240,8 +240,7 @@ azure-pipelines.yml @coq/ci-maintainers /theories/QArith/ @herbelin -/theories/Reals/ @silene -# Secondary maintainer @ppedrot +/theories/Reals/ @coq/reals-library-maintainers /theories/Relations/ @mattam82 # Secondary maintainer @ppedrot |