From eda92eac1659f49894804aa6206990f620fe2389 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 31 May 2018 18:43:11 -0400 Subject: Add codeowner for timing python scripts --- .github/CODEOWNERS | 5 +++++ 1 file changed, 5 insertions(+) (limited to '.github') 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 -- cgit v1.2.3