diff --git a/src/tools/miri/ci/ci.sh b/src/tools/miri/ci/ci.sh index 9d2c3f362e6..4fa0ba8d02d 100755 --- a/src/tools/miri/ci/ci.sh +++ b/src/tools/miri/ci/ci.sh @@ -13,6 +13,15 @@ function endgroup { begingroup "Building Miri" +# Special Windows hacks +if [ "$HOST_TARGET" = i686-pc-windows-msvc ]; then + # The $BASH variable is `/bin/bash` here, but that path does not actually work. There are some + # hacks in place somewhere to try to paper over this, but the hacks dont work either (see + # ). So we hard-code the correct location for Github + # CI instead. + BASH="C:/Program Files/Git/usr/bin/bash" +fi + # Determine configuration for installed build echo "Installing release version of Miri" export RUSTFLAGS="-D warnings" @@ -63,7 +72,7 @@ function run_tests { done # Check that the benchmarks build and run, but without actually benchmarking. - HYPERFINE="bash -c" ./miri bench + HYPERFINE="'$BASH' -c" ./miri bench fi ## test-cargo-miri