Auto merge of #3015 - RalfJung:miri-script, r=RalfJung

rustc-pull: put a newline after the commit ID
This commit is contained in:
bors 2023-08-06 20:46:37 +00:00
commit 7ab10d2098

View File

@ -173,7 +173,7 @@ fn rustc_pull(commit: Option<String>) -> Result<()> {
// the merge has confused the heck out of josh in the past.
// We pass `--no-verify` to avoid running git hooks like `./miri fmt` that could in turn
// trigger auto-actions.
sh.write_file("rust-version", &commit)?;
sh.write_file("rust-version", format!("{commit}\n"))?;
const PREPARING_COMMIT_MESSAGE: &str = "Preparing for merge from rustc";
cmd!(sh, "git commit rust-version --no-verify -m {PREPARING_COMMIT_MESSAGE}")
.run()