|
0b3d8592
|
2018-01-12T11:02:19
|
|
scripts: add backporting script
This adds a simple script for backporting pull requests to older
branches. It accepts as parameters a list of pull request numbers which
whose commits are to be cherry-picked. The identification of PRs
currently happens by using the commit message of the merge of the PR,
which should conform to the message "Merge pull request #<PR>".
While the heuristic works in practice, we could instead also use the
direct references from GitHub via "pull/#<PR>/head". This requires the
user to have all these references fetched, though, so we can just use
the current heuristic until we experience any issues with that.
|