aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github/CODEOWNERS
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-05-31 18:43:11 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-05-31 18:43:11 -0400
commiteda92eac1659f49894804aa6206990f620fe2389 (patch)
tree95df6e9ba234bf7ef2aef1e4f981fbd11156d445 /.github/CODEOWNERS
parent88a632b508977966b1e8d4f4449824a55ffc65d1 (diff)
Add codeowner for timing python scripts
Diffstat (limited to '.github/CODEOWNERS')
-rw-r--r--.github/CODEOWNERS5
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