Checklist for testing and merging a PR

Guidelines to fetch and test a Pull Request (say, PR #200) locally

install the git-pr and git-prw extra Git commands;
cd in the learn-ocaml repository (in the sequel, we assume the remote origin is bound to URL [email protected]:ocaml-sf/learn-ocaml.git);
run git pr 200 origin -f to force-fetch a read-only branch for PR #200,
or git prw 200 origin -f to get a read-and-write branch, i.e., git push will land in the PR-author's work branch.

The CI checks must be green.
Non-trivial PRs should have been tested locally (see the Guidelines above).
Ideally, the commits messages should follow the Conventional Commits guidelines.
This should ease the generation of Release-Notes using release-please.
New user-facing features should be documented within the PR, in directory docs/.

There are 3 PR merging strategies in GitHub (Merge, Merge/Squash, Merge/Rebase).

But for merging PRs, we should rather use Merge or Merge/Squash:

Merge is always a good, standard choice;
Merge/Squash is especially fine if we don't want to keep the commit history of the PR branch or if the PR already contains only one commit;
whereas Merge/Rebase has two drawbacks:
1. there is no mention anywhere of the PR number in the generated commits messages;
2. and the resulting commits are not GPG-signed (cf. the missing Verified badge on those commits).
Actually, Merge/Rebase might be handy in the specific case of "nested PR merging" (namely: we would Merge/Rebase an intermediate PR into a feature branch (for which the intermediate PR number would be useless), then create a subsequent PR, and finally Merge it from the feature branch intoto the master branch itself).