path: root/doc
diff options
authorMartin Schanzenbach <>2021-04-28 10:55:26 +0200
committerMartin Schanzenbach <>2021-04-28 10:55:26 +0200
commit919fd2f427e1a7dda53cd868804d03a61fb0aa87 (patch)
tree276d2d9cf815a6590f5c8a024f2a33d43f1129d9 /doc
parent5c676ddd7e5e36759479b132a42f9af9970bd747 (diff)
-more git handbook
Diffstat (limited to 'doc')
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/handbook/chapters/developer.texi b/doc/handbook/chapters/developer.texi
index 7546f7ac7..24981c020 100644
--- a/doc/handbook/chapters/developer.texi
+++ b/doc/handbook/chapters/developer.texi
@@ -1163,6 +1163,11 @@ Preferably, you would then...
@item (optional) Delete the branch.
@end itemize
+In general, you may want to follow the rule "commit often, push tidy":
+You can create smaller, succinct commits with limited meaning on the commit
+messages. In the end and before you push or merge your branch, you
+can then squash the commits or rename them.
@c ***********************************************************************
@node Build-system
@section Build-system