diff options
| author | XhmikosR <xhmikosr@gmail.com> | 2020-11-01 08:42:19 +0300 |
|---|---|---|
| committer | XhmikosR <xhmikosr@gmail.com> | 2020-11-05 12:22:05 +0300 |
| commit | 39e9cced88428ecdc7206cb4beafcf800993dd2b (patch) | |
| tree | 34a76c62c3f648de7cc7e8952f04c2fd33d685c8 /.github/CONTRIBUTING.md | |
| parent | 30641eb34654899c0f4e87238f775e9ad5bbea5c (diff) | |
Clarify PRs section (#32027)
Diffstat (limited to '.github/CONTRIBUTING.md')
| -rw-r--r-- | .github/CONTRIBUTING.md | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 57619b6eb4..49639a16da 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -124,10 +124,12 @@ Good pull requests—patches, improvements, new features—are a fantastic help. They should remain focused in scope and avoid containing unrelated commits. -**Please ask first** before embarking on any significant pull request (e.g. +**Please ask first** before embarking on any **significant** pull request (e.g. implementing features, refactoring code, porting to a different language), otherwise you risk spending a lot of time working on something that the -project's developers might not want to merge into the project. +project's developers might not want to merge into the project. For trivial +things, or things that don't require a lot of your time, you can go ahead and +make a PR. Please adhere to the [coding guidelines](#code-guidelines) used throughout the project (indentation, accurate comments, etc.) and any other requirements |