about summary refs log tree commit diff
diff options
context:
space:
mode:
-rwxr-xr-xsrc/tools/miri/ci/ci.sh13
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