Skip to content

Commit

Permalink
chore: refine PR template (#3074)
Browse files Browse the repository at this point in the history
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 <scott.morrison@gmail.com>
  • Loading branch information
nomeata and kim-em authored Dec 18, 2023
1 parent 7acbee8 commit 78816a3
Showing 1 changed file with 8 additions and 7 deletions.
15 changes: 8 additions & 7 deletions .github/PULL_REQUEST_TEMPLATE.md
Original file line number Diff line number Diff line change
@@ -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)

0 comments on commit 78816a3

Please sign in to comment.