Re: [boost] [github] default PR destination

Subject: Re: [boost] [github] default PR destination
From: Peter A. Bigot (pab_at_[hidden])
Date: 2014-01-05 10:34:57

On 01/05/2014 08:50 AM, Peter Dimov wrote:
> Peter A. Bigot wrote:
>> The last one (regex) I did off master, and I expect that most future 
>> ones will also be off master.
>
> What is a developer supposed to do with a pull request against master?

Pull the branch to a local repository, merge it into develop, test it, 
and reject or approve it.  Normal git practice: see 
https://help.github.com/articles/merging-a-pull-request under "Merging 
locally".

My point: As a user, I need a working stable tool, so my time goes 
toward creating that.  I'll donate the extra time to submit any solution 
I find back to the project, but I'm not going to donate the hours it'd 
take create/update a developer-oriented workspace and rebuild everything 
just to see whether my patch also works for the developer, who's already 
set up for that sort of thing.

If that's going to be a problem, I'll be happy to skip the 
give-back-to-Boost step.

(for tim: same answer; pull request is never directly merged to master; 
any test farm is not inherently circumvented; etc.)

Peter