Hi Jochen, On 1 Jul 2016 02:07, Jochen Theodorou <[email protected]> wrote:
> no other way to close a pull request... for example one I want not to
> merge? Making dummy commits to
If this is about pull request #124 as well, I'll close it myself today ASAP
and send in a new one as per the comments on that PR :-). Thanks
