chore: make 'impact' a section

This commit is contained in:
mhuisi
2023-09-07 13:35:35 +02:00
committed by Marc Huisinga
parent 7eb3eb189f
commit debd71ec63
2 changed files with 4 additions and 4 deletions

View File

@@ -42,6 +42,6 @@ assignees: ''
[Additional information, configuration or data that might be necessary to reproduce the issue]
### Impact
[Impact: If others are affected by this problem, ask them to add :+1: to this issue. Add :+1: to [other issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc).]
Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others are impacted by this issue, please ask them to add :+1: to it.

View File

@@ -21,6 +21,6 @@ Clear and detailed description of the proposal. Consider the following questions
Ideas should be discussed on [the Lean Zulip](https://leanprover.zulipchat.com) prior to submitting a proposal. Summarize all prior discussions and link them here.
### Impact
[Impact: If others are interested in adding the suggestions from this proposal, ask them to add :+1: to this issue. Add :+1: to [other issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc).]
Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.