From 83556a11206c74cf08291c74614126ce9e57da76 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 22 Aug 2023 20:10:49 +1000 Subject: [PATCH] chore: add PULL_REQUEST_TEMPLATE.md --- .github/PULL_REQUEST_TEMPLATE.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 .github/PULL_REQUEST_TEMPLATE.md 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!