From 78816a3ee7dc2dbb6dd9600a0f2c3f3e1685faf8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 18 Dec 2023 14:47:04 +0100 Subject: [PATCH] chore: refine PR template (#3074) given that we now use the PR description as the commit message, the PR template should point that out. Also, a `# Summary` is relatively strange in a commit message, so removed it. --------- Co-authored-by: Scott Morrison --- .github/PULL_REQUEST_TEMPLATE.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index de549638a553..b5a9b8ac60ca 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -1,13 +1,14 @@ -# Read and remove this section before submitting +# Read this section before submitting * Ensure your PR follows the [External Contribution Guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md). * Please make sure the PR has excellent documentation and tests. If we label it `missing documentation` or `missing tests` then it needs fixing! -* Add the link to your `RFC` or `bug` issue below. +* Include the link to your `RFC` or `bug` issue in the description. * If the issue does not already have approval from a developer, submit the PR as draft. -* Remove this section before submitting. +* The PR title/description will become the commit message. Keep it up-to-date as the PR evolves. +* If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR. +* You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line. +* Remove this section, up to and including the `---` before submitting. -You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line. +--- -# Summary - -Link to `RFC` or `bug` issue: +Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)