diff options
| author | Théo Zimmermann | 2018-12-21 17:15:28 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-21 17:15:28 +0100 |
| commit | 2b067daecb9529cf77a992c76303d1cc85f11537 (patch) | |
| tree | c819526909d8fb617729ee59aaa670f887809ba5 | |
| parent | ee98d818791d8f92674934cda02bfcb3667013c9 (diff) | |
| parent | e515639e16356285517fa8e326ab2823013f7a52 (diff) | |
Merge PR #9266: Make @SkySkimmer an owner of test-suite/report.sh
| -rw-r--r-- | .github/CODEOWNERS | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 0f2dd89975..b0e79fb1b2 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -314,7 +314,7 @@ azure-pipelines.yml @coq/ci-maintainers /test-suite/README.md @gares # Secondary maintainer @SkySkimmer -/test-suite/save-logs @SkySkimmer +/test-suite/report.sh @SkySkimmer /test-suite/complexity/ @herbelin |