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)
Description
Description
Details
Details
- Provenance
Wladimir J. van der Laan <laanwj@gmail.com> Authored on Apr 5 2016, 13:41 schancel Pushed on Jan 5 2018, 21:58 schancel Pushed on Jan 5 2018, 21:39 schancel Pushed on Jan 5 2018, 21:17 - Parents
- rSTAGING10d3ae102afb: devtools: Auto-set branch to merge to in github-merge
rSTAGING214ec0b5e8b2: Merge #7813: [doc] Update port in tor.md - Branches
- Unknown
- Tags
Merged Changes
Merged Changes