I think the tag is the "proper" way to add to the backport list now; I'm not sure anyone is actively watching the user account? We added both at about the same time because we weren't sure what was going to be most convenient. I'm honestly not sure, but since this has sat for a couple of days, let's give it a go.
It is already backported in #11786.
Ah. Guess it didn't crossreference because the only mention of this issue number was in the title?
I watch the julia-backports mailing list, but it's less visible than the label. I prefer people use the label when there's a corresponding issue or pull request that goes along with the proposed backport, and only ping the @juliabackports user for un-attached commits. Or for non-collaborators who don't have permissions to modify issue/pr labels.
I still need to write down my personal backporting policy to make it more formal.
Ah. Guess it didn't crossreference because the only mention of this issue number was in the title?
Right. I always forgot about that, especially when refering a closed issue.... = = ................
If there isn't already an entry for the lack of cross-references from issue/pr titles at https://github.com/isaacs/github/issues, there should be
That doesn't seem like a particularly effective outlet, looking at the closed issue list. Contacting GitHub directly seems like a better choice (and it has worked for me in the past.)