Skip to content

Commit

Permalink
desperate hack: hard-code bash path on Windows
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Mar 24, 2024
1 parent 5b37cd3 commit cd776e2
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion ci/ci.sh
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,15 @@ function run_tests {
done

# Check that the benchmarks build and run, but without actually benchmarking.
HYPERFINE="bash -c" ./miri bench
if [ "$HOST_TARGET" = i686-pc-windows-msvc ]; then
# Some crazy nonsense is going on on Windows where `bash` tries to launch WSL, `$BASH` gets
# replaced to a path that contains a space which ofc breaks becuase HYPERFINE is supposed to
# be shell-encoded, `'$BASH'` does not get the magic replacement and so it refers to a path
# that does not exist... so end result is we have to hard-code the Github CI path here.
HYPERFINE="'C:/Program Files/Git/usr/bin/bash' -c" ./miri bench
else
HYPERFINE="bash -c" ./miri bench
fi
fi

## test-cargo-miri
Expand Down

0 comments on commit cd776e2

Please sign in to comment.