new development tip: please keep merge commits

Proofreading by Thibault Suzanne and Xavier Leroy

(no change entry needed)

HACKING.adoc

@@ -206,6 +206,22 @@ has excellent documentation.
 
 == Development tips and tricks
 
+=== Keep merge commits when merging and cherry-picking Github PRs
+
+Having the Github PR number show up in the git log is very useful for
+later triaging. We recently disabled the "Rebase and merge" button,
+precisely because it does not produce a merge commit.
+
+When you cherry-pick a PR in another branch, please cherry-pick this
+merge-style commit rather than individual commits, whenever
+possible. (Picking a merge commit typically requires the `-m 1`
+option.) You should also use the `-x` option to include the hash of
+the original commit in the commit message.
+
+----
+git cherry-pick -x -m 1 <merge-commit-hash>
+----
+
 === opam compiler script
 
 The separately-distributed script