Hey Francois, I think that since global extensions are not that common anymore that the extra work is not really needed. The important thing about that symbol really is that you know which one takes precedence and is used. Let's get things rolling and this patch in :) All the best. Benni.