max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/.github/PULL_REQUEST_TEMPLATE.md
Denis Gorbachev d126c099f4
doc: Update contribution guides (#2624) 
* doc: update contribution guides

This moves the contribution guide from `doc/contributions.md` to `CONTRIBUTING.md`.
2023-10-25 13:05:55 +11:00

701 B
Raw Blame History

Read and remove this section before submitting

  • Ensure your PR follows the External Contribution Guidelines.
  • 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.
  • If the issue does not already have approval from a developer, submit the PR as draft.
  • Remove this section 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: