Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extend and improve the contribution rules #73

Merged
merged 1 commit into from
Jul 18, 2023
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 16 additions & 5 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,17 @@
Commit rules
============
Rules for branches
==================

When committing to this repository, please follow these rules:
* Use a branch name of the form `⟨type⟩/⟨topic⟩`. Here, `⟨type⟩`
refers to the type of contribution as given by the label of the form
`type: ⟨type⟩` of the pull request associated with the branch.

* For the `⟨topic⟩` part of the branch name, use only lowercase Latin
letters, Arabic numerals, and ASCII dashes, with the latter also
serving as separators of words.


Rules for commits[^original-commit-rules]
=========================================

* Put only related changes into a single commit.

Expand Down Expand Up @@ -38,5 +48,6 @@ When committing to this repository, please follow these rules:
Here, `⟨branch⟩` refers to the name of the branch without the GitHub
account name component.

Several of these rules have been taken from
https://chris.beams.io/posts/git-commit/#seven-rules.
[^original-commit-rules]:
Several of these rules have been taken from
https://chris.beams.io/posts/git-commit/#seven-rules.