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

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