Huh, I think it got merged. Nowadays it's easier to submit stuff through Github. It would be good to ping some core devs about it, or go through Github. I don't want to steal your contribution, but +1 from my side up front.
1 Like