diff options
| author | Ralf Jung <post@ralfj.de> | 2022-10-26 14:01:11 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2022-10-26 14:01:11 +0200 |
| commit | 3986d06542c59e4f826086d6afdd4ce64ab1cd7a (patch) | |
| tree | 69c3e84adb6510a3fee3b7f6a59aab6f3d7dc913 | |
| parent | 6ce5226b4b2b35cb261d92e6ca8622abad28aa6e (diff) | |
test on windows-gnu target
| -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" |