diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-07-27 12:50:19 +0200 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-07-27 12:50:19 +0200 |
| commit | f41557ad13796424692ecca525b58fd03fc9dc7a (patch) | |
| tree | 870618127304b65799e54aa2e45a07398774bfe2 /reproduce/src/make/Top-Makefile | |
| parent | a136e58c5d9a14ea09a13818201848ef98e9c5f9 (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