Subject: Re: [boost] [GitHub] [PR] setting default branch to 'develop'
From: Peter Dimov (lists_at_[hidden])
Date: 2015-10-29 21:25:56
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. :-)