diff options
| author | Maxime Dénès | 2019-03-27 22:51:14 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-27 22:51:14 +0100 |
| commit | a796822e5f57f74ff36e538fd2169f70a8c6c145 (patch) | |
| tree | 56aaff0bd65a945471b27f5fab088aecf4d2459a | |
| parent | 738521ca3acb0f5b87cb1d23360350ed69f18cd1 (diff) | |
| parent | 2fc568a2661907eb6139ec7224fafb8f433aae2b (diff) | |
Merge PR #9827: Move code ownership of reals library to new maintainer team.
Reviewed-by: maximedenes
| -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 |