diff options
| author | Wladimir J. van der Laan <laanwj@gmail.com> | 2017-07-11 15:39:55 +0200 |
|---|---|---|
| committer | Wladimir J. van der Laan <laanwj@gmail.com> | 2017-07-11 15:40:08 +0200 |
| commit | ca4c545cc7e8c06bc8d9d4db1dd2d8f5fe011902 (patch) | |
| tree | a1f2ab55214fc0946f8f52c2c89d38d45d0709c1 /src/Makefile.am | |
| parent | b27b004532dbd91803784cb6beccdfd1aac1b378 (diff) | |
| parent | 475c08cb446371dd75fb37e067613effc0572442 (diff) | |
Merge #10786: Add PR description to merge commit in github-merge.py
475c08c Add PR description to merge commit in github-merge.py (Pieter Wuille)
Pull request description:
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.
Tree-SHA512: cbae46ec24ce911744e11a07e5d51895d3acc79659db306d8124304ef8e422bba99001ee2a741b08c92a5eb39d9c3f6b723622b20d6553ca5cfa0a8de866194c
Diffstat (limited to 'src/Makefile.am')
0 files changed, 0 insertions, 0 deletions