diff options
| author | Maxime Dénès | 2018-06-01 08:40:36 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-01 08:40:36 +0200 |
| commit | dfd7b38d50b28cd2ebd8aa9537f284563add546a (patch) | |
| tree | ee957bcd770af5bedf6bde5e9fe4c1d70b534cbc | |
| parent | 3608fe7c20436095cba1a1a62c89ccc70770dac7 (diff) | |
| parent | eda92eac1659f49894804aa6206990f620fe2389 (diff) | |
Merge PR #7660: Add codeowner for timing python scripts
| -rw-r--r-- | .github/CODEOWNERS | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 782efb5be0..9e87d2ca7a 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 |