There is often some context given in PR descriptions that is missing from commits, and it may be worthwhile to retain that information in our history in git. This PR adds that information to the merge commit when created through github-merge.py
.
We should also encourage people to provide as much information as possible in the PR commits themselves, but I believe that is an orthogonal issue. Individual commits don’t need to have a description of the overall goal of a PR.