On 10/30/2015 04:25 AM, Peter Dimov wrote:
Glen Fernandes wrote:
I understand the motivation, but couldn't we just request from any contributors to submit a new pull request against 'develop' instead of 'master'?
Or, someone with Github connections could try to convince them to add a feature that would allow us to set the default pull request branch separately. :-)
I suspect that would be difficult to do or counter-intuitive. If the default branch is master then the user sees master by default in the web interface, including when he does online edits. When he commits the edits and creates a pull request he has a choice of the target branch. If that branch is develop it is very likely that the PR will have conflicts because he edited master. And that is counter-intuitive because he initially forked from master, so why would the system create a PR for develop? The logical solution for this is to show develop in the web interface by default (thus making edits and PRs on develop by default) and that is what the default branch does.