Re: how to use a different /bin/sh with GNU Make?

[Mark Galeck]

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 <address@hidden>
 To: Mark Galeck <address@hidden> 
Cc: "address@hidden" <address@hidden> 
 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.