diff options
| -rwxr-xr-x | src/tools/miri/miri | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tools/miri/miri b/src/tools/miri/miri index 938df9799da..e21738c3618 100755 --- a/src/tools/miri/miri +++ b/src/tools/miri/miri @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash set -e # Instead of doing just `cargo run --manifest-path .. $@`, we invoke miri-script binary directly. Invoking `cargo run` goes through # rustup (that sets it's own environmental variables), which is undesirable. |