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
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
(for tim: same answer; pull request is never directly merged to master;
any test farm is not inherently circumvented; etc.)
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk