diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 0000000000..59832d5a18 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -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!