From f7a3aa9811aaadbd59b6d399b10f323de7f9647d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 4 May 2024 09:02:51 +0200 Subject: [PATCH] remove a hack that is no longer needed --- src/tools/miri/ci/ci.sh | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/tools/miri/ci/ci.sh b/src/tools/miri/ci/ci.sh index 0db267650db..c8c24ba5da6 100755 --- a/src/tools/miri/ci/ci.sh +++ b/src/tools/miri/ci/ci.sh @@ -13,15 +13,6 @@ 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 - # Global configuration export RUSTFLAGS="-D warnings" export CARGO_INCREMENTAL=0