diff options
author | Wladimir J. van der Laan <laanwj@gmail.com> | 2017-04-26 11:43:52 +0200 |
---|---|---|
committer | Wladimir J. van der Laan <laanwj@gmail.com> | 2017-04-26 11:44:13 +0200 |
commit | bd9ec0ef1ea73209ba9e491e4b7847c895ca7a2f (patch) | |
tree | 249355e44699882915156ef22c8ee776d12f8434 /doc/man | |
parent | 8979f4569e0edaadf883819e2a830379bc1a46df (diff) | |
parent | b508424104c403a9ec12b4adda0d795c2e4d0d6d (diff) |
Merge #9670: contrib: github-merge improvements
b508424 contrib: github-merge improvements (Wladimir J. van der Laan)
Tree-SHA512: 56a34e887716bf6bfcd1b6520f6b9a1bb742e1ad17e75618caf982af71fceb75d50caec1bf4279cb9a2f7a74319f1bcec4c824682841bd6e994acc0991616451
Diffstat (limited to 'doc/man')
0 files changed, 0 insertions, 0 deletions