On Tue, Feb 21, 2012 at 11:03 AM, Christopher Swenson <ch...@caswenson.com> wrote: > My only possible issue with the github workflow: I'm not sure how it > interacts with having multiple people who have control of the "master" > (central) repo. When a pull request comes in, can anyone who has push access > to the repo take control of that pull request?
Yes. Typically one or more core committers participate in the discussion, and it's easy to informally choose who does the final merge. But if you want to be more formal about it, there's an assignee field and a project can choose to use it explicitly and require that person to be the one who does the actual final merge. > Also, in my vastly finite experience with github, I've had problems with the > fact that pull requests seem to be immutable: once a request has been > created, it doesn't seem to be easy to add more commits to it, or change the > commits. (This may just be my naïvety.) No, you can keep pushing to the branch you created the PR from, and new commits show up as they are made. You can even rebase and force push, and the PR will get rebased too. We do the first all the time, and the second also, though less frequently. Cheers, f -- To post to this group, send an email to sage-devel@googlegroups.com To unsubscribe from this group, send an email to sage-devel+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sage-devel URL: http://www.sagemath.org
