chore: add PULL_REQUEST_TEMPLATE.md

This commit is contained in:
Scott Morrison 2023-08-22 20:10:49 +10:00 committed by Leonardo de Moura
parent 24cfae2421
commit 83556a1120

11
.github/PULL_REQUEST_TEMPLATE.md vendored Normal file
View file

@ -0,0 +1,11 @@
* [ ] Put an X in this bracket to confirm you have read the
[External Contribution Guidelines](https://github.com/leanprover/lean4/blob/master/doc/contributions.md).
* Please put the link to your `RFC` or `bug` issue here.
PRs missing this link will be marked as `missing RFC`.
* If that issue does not already have approval from a developer,
please be sure to open this PR in "Draft" mode.
* Please make sure the PR has excellent documentation and tests.
If we label it `missing documentation` or `missing tests` then it needs fixing!