aboutsummaryrefslogtreecommitdiff
path: root/reproduce/src/make/Top-Makefile
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2018-07-27 12:50:19 +0200
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2018-07-27 12:50:19 +0200
commitf41557ad13796424692ecca525b58fd03fc9dc7a (patch)
tree870618127304b65799e54aa2e45a07398774bfe2 /reproduce/src/make/Top-Makefile
parenta136e58c5d9a14ea09a13818201848ef98e9c5f9 (diff)
SHELL has been explicitly set to /bin/bash
On some systems, the default shell `/bin/sh' doesn't point to Bash and this can cause problems and failures when the designer uses its features. Bash (and its extra features) make things very easy and it is very ubiquitous, so it is safe to assume users will have it. This problem was reported by Alejandro Serrano Borlaff.
Diffstat (limited to 'reproduce/src/make/Top-Makefile')
0 files changed, 0 insertions, 0 deletions