diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-05-31 18:43:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-05-31 18:43:11 -0400 |
| commit | eda92eac1659f49894804aa6206990f620fe2389 (patch) | |
| tree | 95df6e9ba234bf7ef2aef1e4f981fbd11156d445 /.github | |
| parent | 88a632b508977966b1e8d4f4449824a55ffc65d1 (diff) | |
Add codeowner for timing python scripts
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 782efb5be..9e87d2ca7 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -307,6 +307,11 @@ /test-suite/coqwc/ @silene # Secondary maintainer @gares +/tools/TimeFileMaker.py @JasonGross +/tools/make-both-single-timing-files.py @JasonGross +/tools/make-both-time-files.py @JasonGross +/tools/make-one-time-file.py @JasonGross + ########## Toplevel ########## /toplevel/ @ejgallego |