Merge to `dev` not `master` / honor the `default branch` setting

Is it possible to configure bors so that it merges to a different branch than “master”? In our project, the default branch is “dev”. Merges to master are only done from dev and are more of release tracking.

Does bors use github’s “default branch” setting to determine the target branch?
If not, is there a config option to change the target branch?
Or is the target branch always taken from the PR itself?

Thanks!
Artur

Yeah, that feature pretty much “just works”. Whichever branch you use as the base of your pull request is the one that bors will merge it into, same way as the Merge Button does.

1 Like

Great, thx! :slight_smile: