push from git gui goes to wrong branch

Hello,

there's a behavior in git gui (v1.7.3.2 and previous) that I consider bugous. Failed to find any bugreporting system on git's website so I'm reporting it here; please correct me if that's wrong.

I have the following snippet in my .git/config:
[branch "article"]
remote = baron
merge = refs/heads/dexen-article

However, the Push' button from git gui sends local branch article' to remote branch article', rather than to the indicated dexen-article'.

For reference, with the CLI git push', the local branch article' is pushed to remote branch `dexen-article' as expected.

Regards,

dexen deVries


``You want to make your way in the CS field? Simple. Calculate rough time of 
amnesia (hell, 10 years is plenty, probably 10 months is plenty), go to the 
dusty archives, dig out something fun, and go for it.   It's worked for many 
people, and it can work for you.''  - Ron Minnich