Fix shebang to be more portable

[wizeman]

On NixOS Linux, make user fails with:

$ make user
scripts/utils/check_for_old_docker_imgs.sh
make: scripts/utils/check_for_old_docker_imgs.sh: No such file or directory
make: *** [Makefile:169: run_checks] Error 127

This is due to scripts/utils/check_for_old_docker_imgs.sh attempting to run bash as its interpreter using a hardcoded /bin/bash path. Unfortunately, this doesn't work on NixOS (as well as some other operating systems) for several reasons, one of them being that bash cannot be installed on /bin, by design.

This PR changes the interpreter path (the shebang directive) to this instead:

#!/usr/bin/env bash

This is a more portable way to run a bash script and is also recommended by numerous sources, including various Stack Overflow answers and even mentioned on Wikipedia (under the "Portability" section): https://en.wikipedia.org/wiki/Shebang_(Unix) . It is also one of the recommended ways to fix this type of issues on NixOS while remaining compatible with other operating systems.

[axel-h]

Thanks. Seem we've done some work in this topic already in other repos

• https://github.com/seL4/seL4/pull/115
• https://github.com/seL4/seL4/pull/511

I wonder if we should do this for all the script here then, not just this one you happened to run into.

[wizeman]

Thanks. I wonder if we should do this for all the script here then, not just this one you happened to run into.

If they are only used inside the docker environment, then I suppose it's not necessary, because they would not need to be portable. But if they're supposed to be ran in the host environment, then I'm guessing that would be a good idea, as long as the interpreter is supposed to be available in $PATH.

But to be honest I can't tell you for sure because I'm not familiar with how they are used, as I'm just using this for the first time, following the instructions from https://docs.sel4.systems/projects/dockerfiles/ . In this scenario, this was the only script that presented this issue for me.

[axel-h]

My understanding was, that docker is a preferred environment, but native execution should also work. So making things more generic makes sense.

[lsf37]

My understanding was, that docker is a preferred environment, but native execution should also work. So making things more generic makes sense.

There are some scripts (in this repos specifically) that run only in their specific docker environment, so they are allowed to make stronger assumptions about what exists and where it is. But using #!/bin/env as a general rule shouldn't hurt, even inside the container.