I'm sorry, I don't have push permissions to repo. I have Sourceware Bugzilla account only. It is my very first patch outside github, so I do not grasp the contributing process very well.