To close a github pr, you have to have a commit that makes it to master with something like "closes #45", where "#45" is the PR number. (Or I think if you merge the exact commit hash from the head of the PR branch that'll work).
https://help.github.com/articles/closing-issues-via-commit-messages/ You can close PRs that are spurious by pushing an empty commit to master with similar language. I usually try to include a reasoning. On Thu, Aug 18, 2016 at 8:53 AM, Aaron D. Mihalik <[email protected]> wrote: > Puja are you still using the "Commit Process for Committers" instructions > at [1]? Can you take a look at these instructions and figure out why they > are not closing the pull requests? > > It would be worth it to see how spark is pulling stuff in. Their PRs look > nice: https://github.com/apache/spark/pull/14695 > > [1] https://cwiki.apache.org/confluence/display/RYA/Contributing+to+Rya > > On Thu, Aug 18, 2016 at 9:14 AM Aaron D. Mihalik <[email protected]> > wrote: > > > Go ahead and pull in changes. That branch is in a bad state and will be > > deleted. Caleb and I will resume the release today. > > > > On Thu, Aug 18, 2016 at 9:00 AM Puja Valiyil <[email protected]> wrote: > > > >> Hey Aaron and Caleb, > >> I saw that there was a release branch. Should we hold off on merging > >> things into develop while you are working on the release? I had put off > >> merging pull requests while you guys were actively working so that it > >> wouldn't be adding work, but there are a lot of requests at this point > >> that > >> should be pulled in. Let me know if its ok to start pulling stuff in or > >> if > >> that will just add more work to what you all are currently doing. > >> Thanks, > >> Puja > >> > > > -- Sean
