mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

when josh-proxy screws up the roundtrip, say what the involved commits are

Browse Source
This commit is contained in:
Ralf Jung 2024-08-01 12:26:17 +02:00
parent 50d51fb1bf
commit 91175463e4
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/tools/miri/miri-script/src/commands.rs
View File

@ -355,7 +355,10 @@ impl Command {
let head = cmd!(sh, "git rev-parse HEAD").read()?; let head = cmd!(sh, "git rev-parse HEAD").read()?;
let fetch_head = cmd!(sh, "git rev-parse FETCH_HEAD").read()?; let fetch_head = cmd!(sh, "git rev-parse FETCH_HEAD").read()?;
if head != fetch_head { if head != fetch_head {
bail!("Josh created a non-roundtrip push! Do NOT merge this into rustc!"); bail!(
"Josh created a non-roundtrip push! Do NOT merge this into rustc!\n\
Expected {head}, got {fetch_head}."
);
} }
println!( println!(
"Confirmed that the push round-trips back to Miri properly. Please create a rustc PR:" "Confirmed that the push round-trips back to Miri properly. Please create a rustc PR:"