diff options
| -rw-r--r-- | src/tools/miri/miri-script/src/commands.rs | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/tools/miri/miri-script/src/commands.rs b/src/tools/miri/miri-script/src/commands.rs index be0fdbc177a..57bdfbad9af 100644 --- a/src/tools/miri/miri-script/src/commands.rs +++ b/src/tools/miri/miri-script/src/commands.rs @@ -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()?) }; |