Please fix bash shebangs in scripts

[yurivict]

For example, the file examples/reduced_basis/reduced_basis_ex6/run.sh has "#!/bin/bash" and the correct shebang is "#!/usr/bin/env bash".

On BSDs and some other systems bash isn't in /bin/bash and it should be resolved through the PATH variable.

[roystgnr]

That's a good idea, for scripts where we do need bash ... although I'll bet there's a lot more of our scripts (possibly all of them?) where either we don't need bash or we accidentally introduced bash-isms out of laziness. We should probably stop requiring bash rather than sh for those.

2 questions:

Is #!/usr/bin/env sh still the best shebang in that case? I see that sh isn't guaranteed to be in /bin by POSIX, but it seems like that's probably a safer bet than env being in /usr/bin.

Is there a better alternative to dash for testing POSIX compliance? That's /bin/sh on Ubuntu and the package literally calls it "POSIX-compliant shell", but I'm reading (and verifying) that dash still supports some non-POSIX idioms I use habitually like echo -n.

[yurivict]

Is #!/usr/bin/env sh still the best shebang in that case?

No, "#!/bin/sh" should suffice.

Is there a better alternative to dash for testing POSIX compliance?

ShellCheck is supposed to be a good way to check POSIX compatibility. This StackExchange answer suggests the same.

Additionally, FYI, in case you didn't know, shell interpreters support the "STRICT" mode when they don't tolerate some borderline erroneous behavior of the code.

The STRICT mode can be turned on with this command: set -euo pipefail

I think you should use it in all shell scripts.

[jwpeterson]

This should be fixed in master (#3996), branch_v1.8.0, and I also back-ported the changes to the 1.7.x release branch.