diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index c6155a4163..560d696a1f 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -52,6 +52,10 @@ PR Submission:
 
 **Descriptive Title and Summary**: The PR title should briefly explain the purpose of the PR. The summary should give more detailed information on what changes are made and why. Links to Zulip threads are not acceptable as a summary. You are responsible for summarizing the discussion, and getting support for it.
 
+**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](https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md). 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.
+
 **Link to Relevant Issues**: Reference any issues that your PR addresses to provide context.
 
 **Stay Responsive**: Once the PR is submitted, stay responsive to feedback and be prepared to make necessary revisions. We will close any PR that has been inactive (no response or updates from the submitter) for more than a month.
diff --git a/doc/dev/commit_convention.md b/doc/dev/commit_convention.md
index 04a82f7c7e..80362c175b 100644
--- a/doc/dev/commit_convention.md
+++ b/doc/dev/commit_convention.md
@@ -1,10 +1,15 @@
 Git Commit Convention
 =====================
 
-We are using the following convention for writing git-commit messages.
-It is based on the one from AngularJS project([doc][angularjs-doc],
+We are using the following convention for writing git commit messages. For pull
+requests, make sure the pull request title and description follow this
+convention, as the squash-merge commit will inherit title and body from the
+pull request.
+
+This convention is based on the one from the AngularJS project ([doc][angularjs-doc],
 [commits][angularjs-git]).
 
+
 [angularjs-git]: https://github.com/angular/angular.js/commits/master
 [angularjs-doc]: https://docs.google.com/document/d/1QrDFcIiPjSLDn3EL15IJygNPiHORgU1_OOAqWjiDU5Y/edit#