Skip to content

Commit

Permalink
Auto merge of #3174 - RalfJung:rustc-git, r=RalfJung
Browse files Browse the repository at this point in the history
miri script: fix RUSTC_GIT error message

Making this a flag is tricky since our command-line parsing is pretty crude.

Fixes #3173
  • Loading branch information
bors committed Nov 18, 2023
2 parents 133e989 + 7bdb56d commit 02baccc
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion miri-script/src/commands.rs
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,7 @@ impl Command {
"This will pull a copy of the rust-lang/rust history into this Miri checkout, growing it by about 1GB."
);
print!(
"To avoid that, abort now and set the `--rustc-git` flag to an existing rustc checkout. Proceed? [y/N] "
"To avoid that, abort now and set the `RUSTC_GIT` environment variable to an existing rustc checkout. Proceed? [y/N] "
);
std::io::stdout().flush()?;
let mut answer = String::new();
Expand Down

0 comments on commit 02baccc

Please sign in to comment.