It appears I'm no longer able to close tickets here after the move, but i have just pushed the missing commit to github. Sorry!
You can send pull requests through github indeed, I'll make sure it ends up in the sf svn repo too. (It should be possible to merge the pull request and then immediately push it to the svn repo. I might however have to force push back to github to keep sync with the exact svn commit. This will be first, so a test, lets see what happens..) Thanks!
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
It appears I'm no longer able to close tickets here after the move, but i have just pushed the missing commit to github. Sorry!
You can send pull requests through github indeed, I'll make sure it ends up in the sf svn repo too. (It should be possible to merge the pull request and then immediately push it to the svn repo. I might however have to force push back to github to keep sync with the exact svn commit. This will be first, so a test, lets see what happens..) Thanks!
Thanks, appreciated!
This is not a bug ... :)