Recommend to amend pull requests

timhoffm · timhoffm · commit 45f2d5fcb19d · 2020-02-16T19:50:11.000+01:00
diff --git a/doc/devel/coding_guide.rst b/doc/devel/coding_guide.rst
@@ -32,6 +32,12 @@ When making a PR, pay attention to:
   feedback from the developers. You may mark these as
   `draft pull requests <https://help.github.com/en/articles/about-pull-requests#draft-pull-requests>`_
   on GitHub.
+* When updating your PR, instead of adding new commits to fix something, please
+  consider amending your initial commit(s) to keep the history clean.
+  (You can achieve this using::
+
+      git commit --amend --no-edit
+      git push origin [yourbranch] --force
 
 See also :ref:`contributing` for how to make a PR.
 
