diff options
| author | Théo Zimmermann | 2019-03-25 16:32:40 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-25 16:32:40 +0100 |
| commit | 2fc568a2661907eb6139ec7224fafb8f433aae2b (patch) | |
| tree | 9d55ada43329571013b5f49d5610d1cb78522509 /.github | |
| parent | fd065eae52dde32bcb95955f6da9280fed780729 (diff) | |
Move code ownership of reals library to new maintainer team.
Diffstat (limited to '.github')
| -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 |