From 91175463e4168d3e100a9668a62ca0d0b97e7ba3 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 1 Aug 2024 12:26:17 +0200 Subject: [PATCH] when josh-proxy screws up the roundtrip, say what the involved commits are --- src/tools/miri/miri-script/src/commands.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tools/miri/miri-script/src/commands.rs b/src/tools/miri/miri-script/src/commands.rs index 62a3ab2c34c..fc205040baf 100644 --- 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:"