build: Prefer /bin/bash if available. Thanks, Vagrant!
authorJan Nieuwenhuizen <janneke@gnu.org>
Sat, 9 Nov 2019 09:59:01 +0000 (10:59 +0100)
committerJan Nieuwenhuizen <janneke@gnu.org>
Sat, 9 Nov 2019 09:59:01 +0000 (10:59 +0100)
commit11798d4272002a00d7e07112caf0757e2043afd1
treefaf1ae8b1fed990dbd45286a4a531c598afc0f84
parentc6cceb47f32e24f7502cfb91604f2eb318dfd683
build: Prefer /bin/bash if available. Thanks, Vagrant!

Ensure the configure script uses /bin/bash, otherwise on systems with
/bin -> /usr/bin it results in /bin/bash being embedded in various
scripts.

Inspired by

    https://salsa.debian.org/debian/mes/blob/debian/master/debian/patches/force-use-of-bin-bash

* configure: Prefer /bin/bash, /bin/sh if available.  Helps
reproducibility on Debian.
configure