Clarify PRs section (#32027)

diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md
index 0055f2207844a773d5316f51e17715edf052a511..0913b5b5be1bc7cff2497c39d4ae8c901d2596d1 100644 (file)
--- a/.github/CONTRIBUTING.md
+++ b/.github/CONTRIBUTING.md
@@ -123,10 +123,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