aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-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