Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
devtools: Auto-set branch to merge to in github-merge #7781
As we are already using the API to retrieve the pull request title, also retrieve the base branch.
This makes sure that pull requests for 0.12 automatically end up in 0.12, and pull requests for master automatically end up in master, and so on.
It prints the branch it is about to merge into. It is still possible to override the branch from the command line or using the