Skip to content

Commit

Permalink
fix './miri run --dep --target _'
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed May 26, 2024
1 parent 331bb3f commit cbec128
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/tools/miri/miri-script/src/commands.rs
Original file line number Diff line number Diff line change
Expand Up @@ -531,7 +531,13 @@ impl Command {
};
cmd.set_quiet(!verbose);
// Add Miri flags
let cmd = cmd.args(&miri_flags).args(&seed_flag).args(&early_flags).args(&flags);
let mut cmd = cmd.args(&miri_flags).args(&seed_flag).args(&early_flags).args(&flags);
// For `--dep` we also need to set the env var.
if dep {
if let Some(target) = &target {
cmd = cmd.env("MIRI_TEST_TARGET", target);
}
}
// And run the thing.
Ok(cmd.run()?)
};
Expand Down

0 comments on commit cbec128

Please sign in to comment.