Re: [boost] [GitHub] [PR] setting default branch to 'develop'

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. :-)