f91ab0ccb7
ci: support cherry-picking of merge PRs
...
This change assumes that it is always safe to use the first commit
parent as the mainline. I believe this assumption is safe with a
github merge workflow.
2020-03-18 12:38:04 -04:00
3e0ecc096c
cherry pick 'docs-cherrypick' label rather than 'docs' to stable-website ( #7443 )
2020-03-12 13:22:51 -04:00
2622f2644a
add Authorization header in GitHub API call ( #7436 )
2020-03-11 13:25:15 -04:00
bd951c7023
set pr_url outside if ( #7424 )
2020-03-10 12:31:58 -04:00
740bee5928
add slack notifications for cherry-pick ( #7423 )
2020-03-10 11:47:23 -04:00
c2b5edf805
add auto cherry-picking ( #7406 )
...
* add auto cherry-picking
* exit on git cherry-pick failure
* release branches are #.#.x
2020-03-06 17:59:14 -05:00
Daniel Nephin