Ah, so right. My apologies for not doing deeper research. I'll take a more complete look later today.
On Thu, Dec 4, 2014 at 3:12 AM, Federico Bruni <f...@inventati.org> wrote: > Il giorno gio 4 dic 2014 alle 8:00, Glen Larsen <glenl....@gmail.com> ha > scritto: > > These instructions are modifying an inactive pull request. Looking at the > first section about modifying an *active* pull request locally it > mentions following commands given at the bottom of a pull request. > > > Right, but only collaborators can merge a pull request through github. > On the bottom of any pull request I can see only: > > > This pull request can be automatically merged by project collaborators. > > Only those with write access to this repository can merge pull requests. > >
_______________________________________________ Mutopia-discuss mailing list Mutopia-discuss@mutopiaproject.org http://lists.bcn.mythic-beasts.com/mailman/listinfo/mutopia-discuss
