Re: closing pull requests without merge

[Roman Shaposhnik <ro...@shaposhnik.org>]

On Thu, Jun 30, 2016 at 1:37 PM, Jochen Theodorou <bl...@gmx.org> wrote:
> Hi all,
>
> I know I can close a github pull request using a commit message, and I know
> we cannot do it using the UI (as long as I am not the author of the request
> at least), because it is a read-only mirror. But is there really no other
> way to close a pull request... for example one I want not to merge? Making
> dummy commits to master is not really a good thing. Afaik making a commit to
> another branch won't close it

The only two other ways I know of are:
   1. asking the original submitter to close it
   2. have a dummy commit with a message closing a bunch of PRs

Thanks,
Roman.