diff options
| author | Gaëtan Gilbert | 2020-08-25 09:06:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-25 09:06:45 +0200 |
| commit | 1b2d2bdaa44798377fb2e853278013621140e6d5 (patch) | |
| tree | 99a1a7510e0da7b7f1dcc72f8af7ee82d3d70e35 /.github | |
| parent | 016bafd7519859737610810df77f72bf812c542a (diff) | |
Add /dev/bench to CODEOWNERS
Diffstat (limited to '.github')
| -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 |