diff options
author | Wladimir J. van der Laan <laanwj@gmail.com> | 2016-04-05 15:41:13 +0200 |
---|---|---|
committer | Wladimir J. van der Laan <laanwj@gmail.com> | 2016-04-05 15:41:34 +0200 |
commit | 55db5f07b1c4e82181f691725212587fcafd6f2a (patch) | |
tree | 183cc8b746a7b7f6a305e6acf7115fe5a61d3da7 /src | |
parent | 214ec0b5e8b2d27418aac3226954381151da19d9 (diff) | |
parent | 10d3ae102afb89b3f50cd27f9ee657e5a542eb1b (diff) |
Merge #7781: devtools: Auto-set branch to merge to in github-merge
10d3ae1 devtools: Auto-set branch to merge to in github-merge (Wladimir J. van der Laan)
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions