Given that some OSes have bash in /usr/local/bin and in order not to
give too easy an excuse to Olivier for not backporting fixes, let's
make a few scripts rely on /usr/bin/env bash instead of /bin/bash :-)
These ones have been used for several months already and are quite
convenient to emit new releases and backport fixes. I'm fed up with
having different versions on different machines, let's commit them
now.