Allow building the documentation with make in systems without /bin/bash

[Gallaecio]

595146e#r48800250

I’m guessing the current code exists in line with https://stackoverflow.com/a/589300/939364, in order to force Bash to be used (instead of something like sh).

If there is a way to set SHELL to Bash so that it finds the right path to Bash regardless of the system, that would be great. Otherwise, maybe we can check if there is any Bash-specific code in this Makefile. If all commands work as intended with sh, for example, maybe we can just remove this line as suggested.

[apalala]

How about this?

BASH=`which bash`

[Gallaecio]

The approach in #5082 sounds good, in modern scripting #!/usr/bin/env bash is often the recommended line to put at the beginning of a Bash script. I haven’t approved it yet because I want to test it manually first.