diff options
| author | Ralf Jung <post@ralfj.de> | 2024-08-01 12:26:17 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2024-08-01 12:26:32 +0200 |
| commit | 91175463e4168d3e100a9668a62ca0d0b97e7ba3 (patch) | |
| tree | 535c142b33f4e9b575debe4fe7dc03a56007c3a7 | |
| parent | 50d51fb1bfee724a8daefd1fa4921ae36600e61f (diff) | |
| download | rust-91175463e4168d3e100a9668a62ca0d0b97e7ba3.tar.gz rust-91175463e4168d3e100a9668a62ca0d0b97e7ba3.zip | |
when josh-proxy screws up the roundtrip, say what the involved commits are
| -rw-r--r-- | src/tools/miri/miri-script/src/commands.rs | 5 |
1 files changed, 4 insertions, 1 deletions
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:" |