Am 07.07.2014 13:57, schrieb "Nordlöw":
On Monday, 7 July 2014 at 11:55:48 UTC, Nordlöw wrote:
BTW, corresponding GitHub issue:

Do you fix the PR?

Shall I just commit the file (with you as the author of course), or do you want to open a pull request?

I've tried it now and it worked flawlessly so far.

Reply via email to