remove a hack that is no longer needed
This commit is contained in:
parent
6ce00aa992
commit
f7a3aa9811
@ -13,15 +13,6 @@ function endgroup {
|
|||||||
|
|
||||||
begingroup "Building Miri"
|
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
|
|
||||||
# <https://github.com/rust-lang/miri/pull/3402>). So we hard-code the correct location for Github
|
|
||||||
# CI instead.
|
|
||||||
BASH="C:/Program Files/Git/usr/bin/bash"
|
|
||||||
fi
|
|
||||||
|
|
||||||
# Global configuration
|
# Global configuration
|
||||||
export RUSTFLAGS="-D warnings"
|
export RUSTFLAGS="-D warnings"
|
||||||
export CARGO_INCREMENTAL=0
|
export CARGO_INCREMENTAL=0
|
||||||
|
Loading…
Reference in New Issue
Block a user