Auto merge of rust-lang#3782 - RalfJung:josh-roundtrip-error, r=RalfJung

when josh-proxy screws up the roundtrip, say what the involved commits are
RalfJung · Aug 1, 2024 · 9de5630 · 9de5630
2 parents 769e900 + 9117546
commit 9de5630
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/tools/miri/miri-script/src/commands.rs b/src/tools/miri/miri-script/src/commands.rs
@@ -355,7 +355,10 @@ impl Command {
         let head = cmd!(sh, "git rev-parse HEAD").read()?;
         let fetch_head = cmd!(sh, "git rev-parse FETCH_HEAD").read()?;
         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!(
             "Confirmed that the push round-trips back to Miri properly. Please create a rustc PR:"