diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 5 | ||||
| -rw-r--r-- | .github/PULL_REQUEST_TEMPLATE.md | 3 |
2 files changed, 8 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 diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 86c15f6e80..4a8606a38a 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -10,6 +10,9 @@ Fixes / closes #???? +<!-- If there is a user-visible change in coqc/coqtop/coqchk/coq_makefile behavior and testing is not prohibitively expensive: --> +<!-- (Otherwise, remove this line.) --> +- [ ] Added / updated test-suite <!-- If this is a feature pull request / breaks compatibility: --> <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). |