diff options
| author | Ralf Jung <post@ralfj.de> | 2025-02-24 10:57:57 +0100 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2025-02-24 13:22:13 +0100 |
| commit | 561dce772fed55a73f474b2e3f79c43981ea084f (patch) | |
| tree | 257c4f3a4f442c27920a056833e3db7d62996f02 | |
| parent | bba96636213e996d712454f24e4b08abf105835f (diff) | |
| download | rust-561dce772fed55a73f474b2e3f79c43981ea084f.tar.gz rust-561dce772fed55a73f474b2e3f79c43981ea084f.zip | |
sanity-check for HOST_TARGET
| -rwxr-xr-x | src/tools/miri/ci/ci.sh | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/tools/miri/ci/ci.sh b/src/tools/miri/ci/ci.sh index 5583030b490..3327ad17c44 100755 --- a/src/tools/miri/ci/ci.sh +++ b/src/tools/miri/ci/ci.sh @@ -1,5 +1,5 @@ #!/bin/bash -set -euo pipefail +set -eu function begingroup { echo "::group::$@" @@ -11,6 +11,17 @@ function endgroup { echo "::endgroup" } +begingroup "Sanity-check environment" + +# Ensure the HOST_TARGET is what it should be. +if ! rustc -vV | grep -q "^host: $HOST_TARGET\$"; then + echo "This runner should be using host target $HOST_TARGET but rustc disagrees:" + rustc -vV + exit 1 +fi + +endgroup + begingroup "Building Miri" # Global configuration |
