diff options
| author | bors <bors@rust-lang.org> | 2024-02-24 16:30:37 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2024-02-24 16:30:37 +0000 |
| commit | 2f1c9db3cf34593b93048060a00e13b325b64283 (patch) | |
| tree | afbb6a61fbdc01c7500a0d6dea45d988b82d4e58 /src | |
| parent | 40dc2b4bd2dfe7a9f03cec85657425d2746d4f50 (diff) | |
| parent | c7be4439ade7cd4b1e506bd87f2c9b131c6d594e (diff) | |
Auto merge of #3316 - RossSmyth:windows-script, r=RalfJung
Windows miri-script execution egronomics
This allows for Windows users to use miri-script without pain. As working on miri earlier I was doing
`.\miri-script\target\debug\miri-script.exe { install | build | ... }` which wasn't fun.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tools/miri/miri.bat | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/tools/miri/miri.bat b/src/tools/miri/miri.bat new file mode 100644 index 00000000000..91e8a6e8f3b --- /dev/null +++ b/src/tools/miri/miri.bat @@ -0,0 +1,10 @@ +:: This makes execution of ./miri on Linux and Windows the same. +:: Windows will not execute the bash script, and select this. +@echo off +set MIRI_SCRIPT_TARGET_DIR=%0\..\miri-script\target +cargo build %CARGO_EXTRA_FLAGS% -q --target-dir %MIRI_SCRIPT_TARGET_DIR% --manifest-path %0\..\miri-script\Cargo.toml + +:: Forwards all arguments to this file to the executable. +:: We invoke the binary directly to avoid going through rustup, which would set some extra +:: env vars that we do not want. +%MIRI_SCRIPT_TARGET_DIR%\debug\miri-script %* |