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?