1. 12 Jan, 2018 1 commit
    • scripts: add backporting script · 0b3d8592
      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.
      Patrick Steinhardt committed