rust-lang
Include repo name in merge commit message?
Both Clippy and Miri use some sort of tooling to reflect their own local history into the rustc repo, preserving individual commits. This unfortunately means that when bors creates a Miri merge commit like "Auto merge of #2636 - RalfJung:scalar-field-retag, r=oli-obk", when that commit gets put into the rustc repo, Github interprets #2636 as a rustc PR number, which of course leads to bogus links.
Would it be possible for bors to create these commit messages in a way that the links will keep working when the message is put into a different repo, at least within the rust-lang org?
Neither homu nor bors is planned to be used for subtrees anymore, so this is not relevant anymore. Sure would be nice if GitHub allowed us to put the repo name in the merge queue commit message..
It is still relevant in the other direction -- Miri's history is full of rustc commits saying "auto merge of #foo" and github tries to interpret those as Miri issue numbers when they actually are rustc issue numbers.
Ah, right, I forgot about that. But the chance of rustc commits actually closing an issue in a subtree is relatively low, no? The difference in numbers is ~100k.
This isn't about closing anything, it's about where the link goes. There are two problems:
- As Miri PR numbers go up, old rustc PRs reflected in Miri history will slowly start getting hyperlinked by rustc.
- Current rustc PRs in Miri are not hyperlinked at all so I have to follow the PR number manually.
Hmm, ok. I'll reopen the issue, but doing this change would require going through several tools and making sure that they can parse both the old and the new formats, so it should probably be left as a follow-up to be done some time after we actually start using new bors for merges, to avoid too many changes at once.