It appears that the git repository is one change behind the svn one.
I have a patch to upstream, can I do that via the github web UI?
Diederick C. Niehorster
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!
This is not a bug ... :)