Clarify PRs section (#32027)

diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md
index 57619b6eb4f6db7e1f677707737bd30f80371058..49639a16da826e95ec2c3d09be12c0129e44180c 100644 (file)
--- 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