diff options
| author | coqbot-app[bot] | 2020-08-25 12:40:30 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-25 12:40:30 +0000 |
| commit | 60684d29ed02e0879d94171943920a0324172a7b (patch) | |
| tree | ddf9c355a85308b83e47e9602a956514ac523bb5 | |
| parent | ae712c6460cc400eda3188d59baf5d69b93ad70a (diff) | |
| parent | 1b2d2bdaa44798377fb2e853278013621140e6d5 (diff) | |
Merge PR #12888: Add /dev/bench to CODEOWNERS
Reviewed-by: Zimmi48
| -rw-r--r-- | .github/CODEOWNERS | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index c4d202470d..bb0beb142a 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -34,6 +34,8 @@ # Trick to avoid getting review requests # each time someone adds an overlay +/dev/bench/ @coq/bench-maintainers + ########## Documentation ########## /README.md @coq/doc-maintainers |