Skip to content

Commit 782bc54

Browse files
committed
Auto merge of #3782 - RalfJung:josh-roundtrip-error, r=RalfJung
when josh-proxy screws up the roundtrip, say what the involved commits are
2 parents cc70cad + 5e5cff2 commit 782bc54

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

miri-script/src/commands.rs

+4-1
Original file line numberDiff line numberDiff line change
@@ -355,7 +355,10 @@ impl Command {
355355
let head = cmd!(sh, "git rev-parse HEAD").read()?;
356356
let fetch_head = cmd!(sh, "git rev-parse FETCH_HEAD").read()?;
357357
if head != fetch_head {
358-
bail!("Josh created a non-roundtrip push! Do NOT merge this into rustc!");
358+
bail!(
359+
"Josh created a non-roundtrip push! Do NOT merge this into rustc!\n\
360+
Expected {head}, got {fetch_head}."
361+
);
359362
}
360363
println!(
361364
"Confirmed that the push round-trips back to Miri properly. Please create a rustc PR:"

0 commit comments

Comments
 (0)