According to the GNU Make manual, the shell that is used to spawn recipe lines,
is the value of Make variable $(SHELL) which is by default /bin/sh, unless it
is changed in a Makefile.
That is not to be confused of course with the parent shell variable $SHELL,
which is something else altogether, and yes, it is /bin/bash on my machine too.
From: Tim Murphy <tnmur...@gmail.com>
To: Mark Galeck <mark_gal...@pacbell.net>
Cc: "help-make@gnu.org" <help-make@gnu.org>
Sent: Tuesday, October 13, 2015 2:55 AM
Subject: Re: how to use a different /bin/sh with GNU Make?
/bin/sh is a link to /bin/bash on my machine
if you type echo $SHELL at the commandline what comes up? for me it's
"/bin/bash"
i.e. changing /bin/sh might not be helping you if your make is using
bash just because of the environment setting.
_______________________________________________
Help-make mailing list
Help-make@gnu.org
https://lists.gnu.org/mailman/listinfo/help-make
