From 5864245d89b664fce9014bea811e6e6720dd949d Mon Sep 17 00:00:00 2001 From: Nilstrieb <48135649+Nilstrieb@users.noreply.github.com> Date: Fri, 8 Sep 2023 22:30:50 +0200 Subject: [PATCH] Use `#!/usr/bin/env` shebang MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ``` $ ls /bin/bash ls: cannot access '/bin/bash': No such file or directory ``` On certain systems, `/bin` and `/usr/bin` are nothing but wastelands, with just `env`around as the last survivor of the great purge. The binaries have cowardly hidden away and only `env` can show us the way to greatness (bash). ❄️ --- src/tools/miri/miri | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tools/miri/miri b/src/tools/miri/miri index 938df9799da3..e21738c36184 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.