On 2016-02-11 12:13 PM, Stephen E. Baker wrote:
> I have set master as a protected branch in github. This means no one
> will be able to delete it or force push to it. Only pull requests that
> have passed their Travis and AppVeyor checks will be able to be
> merged, except by the project owners.
William brought up the point that this means we will not be able to fix
up other people's pull requests and merge them directly. In a way this
is good, since the changes have not been checked, there is the potential
that they could break the master build. On the other hand, it is
inconvenient when some of our contributors do not know how manage git
In the mean time I've suggested the following escalation of action:
Request that the owner of the pull request make the changes (e.g.
If they are unable to do it themselves, request commit access to their
public repository and make the changes in the branch the pull request is
If they cannot or will not give us permission to access their repository
then we (the reviewer) will pull the changes into our own public repo,
close the existing pull request and open a new one.
If this turns out to be too much of a burden I will disable the
requirement for appveyor and travis checks.