Repository navigation
miri no longer builds after rust-lang/rust#63575 #63581
Description
Hello, this is your friendly neighborhood mergebot.
After merging PR #63575, I observed that the tool miri no longer builds.
A follow-up PR to the repository https://github.com/rust-lang/miri is needed to fix the fallout.
cc @Centril, do you think you would have time to do the follow-up work?
If so, that would be great!
cc @Centril, the PR reviewer, and @rust-lang/compiler -- nominating for prioritization.
This issue has been assigned to @lzutao via this comment.
Activity
nikomatsakis commentedon Aug 15, 2019
Compiler team triage: marking as P-high, as miri should build. @RalfJung, @oli-obk -- any idea what it takes to fix this?
RalfJung commentedon Aug 15, 2019
It's already fixed in the Miri repo. Just takes someone to do the PR for rustc.
@lzutao do you want to do that?
Also @nikomatsakis, in the past we treated these as P-medium. Ultimately of course this is up to the compiler team, I personally will always treat it as high priority to keep at least the Miri repo itself working.
nikomatsakis commentedon Aug 15, 2019
OK. I think it ought to be high priority to keep things building, personally, but I'm happy to defer to convention for now, as we have too many P-high bugs ultimately.
tesuji commentedon Aug 15, 2019
@rustbot claim
Auto merge of #63596 - lzutao:update-miri, r=RalfJung