You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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?
The text was updated successfully, but these errors were encountered:
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?
The text was updated successfully, but these errors were encountered: