diff options
Diffstat (limited to 'src')
| -rwxr-xr-x | src/tools/miri/ci.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tools/miri/ci.sh b/src/tools/miri/ci.sh index aa322e54a31..72b7b791a47 100755 --- a/src/tools/miri/ci.sh +++ b/src/tools/miri/ci.sh @@ -93,6 +93,7 @@ case $HOST_TARGET in ;; i686-pc-windows-msvc) MIRI_TEST_TARGET=x86_64-unknown-linux-gnu run_tests + MIRI_TEST_TARGET=x86_64-pc-windows-gnu run_tests ;; *) echo "FATAL: unknown OS" |