diff options
Diffstat (limited to '.github/CODEOWNERS')
| -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 |