diff options
Diffstat (limited to '.github')
-rw-r--r-- | .github/ISSUE_TEMPLATE.md | 18 | ||||
-rw-r--r-- | .github/PULL_REQUEST_TEMPLATE.md | 16 |
2 files changed, 34 insertions, 0 deletions
diff --git a/.github/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE.md new file mode 100644 index 00000000..c9cb516c --- /dev/null +++ b/.github/ISSUE_TEMPLATE.md @@ -0,0 +1,18 @@ +<!-- Thank you for your contribution. + Please complete the following information when reporting a bug. --> + +#### Version + +<!-- You can get this information by running `coqtop -v`. --> + + +#### Operating system + + +#### Description of the problem + +<!-- It is helpful to provide enough information so that we can reproduce the bug. + In particular, please include a code example which produces it. + If the example is small, you can include it here between ``` ```. + Otherwise, please provide a link to a repository, a gist (https://gist.github.com) + or drag-and-drop a `.zip` archive. --> diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 00000000..a9230042 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -0,0 +1,16 @@ +<!-- Thank you for your contribution. + Make sure you read the contributing guide and fill this template. --> + + +<!-- Keep what applies --> +**Kind:** documentation / bug fix / feature / performance / infrastructure. + + +<!-- If this is a bug fix, make sure the bug was reported beforehand. --> +Fixes / closes #???? + + +<!-- If this is a feature pull request / breaks compatibility: --> +<!-- (Otherwise, remove these lines.) --> +- [ ] Corresponding documentation was added / updated. +- [ ] Entry added in CHANGES. |