Skip to content

Commit

Permalink
doc: add CONTRIBUTING.md (#22)
Browse files Browse the repository at this point in the history
Add CONTRIBUTING.md with links to the PR Submission section of lean4's
CONTRIBUTING.md and lean4's commit_convention.md.
  • Loading branch information
austinletson authored May 15, 2024
1 parent c91e70b commit 0fe2957
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
## Contribution Guidelines
Follow Lean's [Commit Convention](https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md).

For more information see the [PR Submission](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md#pr-submission) section in lean4's CONTRIBUTING.md.

Note this key detail:
> Follow the commit convention: Pull requests are squash merged, and the commit message is taken from the pull request title and body, so make sure they adhere to the commit convention. Put questions and extra information, which should not be part of the final commit message, into a first comment rather than the Pull Request description. Because the change will be squashed, there is no need to polish the commit messages and history on the branch.

0 comments on commit 0fe2957

Please sign in to comment.