I'll import it to github. This will have to wait until tomorrow though, as it's too late now. I don't know how github permissions thing works but I'll check how I can give you push rights. What's your username over there?