Comment 4 for bug 732035

Just wondering was this commit really merged into master branch? Can someone post link to the git commit. Looking from above posts it looks like Oliver has committed code to his personal branch and made a pull request on 2012-05-13. Adolfo changed status to "Fix Committed" on 2012-06-09. If this is only commit to personal branch this status is wrong. "Fix
Committed" status should only be assigned if commit is done to the master branch and so it will be available to end-users in next release. So is this really fixed or just wrongly tagged?