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

[Mark Galeck]

Yes David you are right, I missed that somehow...  I thought, the manual says 
you can't have SHELL value from the environment, so that "meant" you always 
have to repeat the assignment SHELL=$(SHELL).  I read this on Stack Overflow 
some time ago and did not think about it.  
But yes somehow the simple assignment SHELL=<changed shell> on the top-level 
make comamnd line, does propagate.  
Thank you!
      From: David Boyce <address@hidden>
 To: Mark Galeck <address@hidden> 
Cc: Reinier Post <address@hidden>; "address@hidden" <address@hidden> 
 Sent: Tuesday, October 13, 2015 12:23 PM
 Subject: Re: how to use a different /bin/sh with GNU Make?
   
I haven’t followed this whole thread, so apologies if I missed
something, but you should be able to simply override SHELL on the
command line and it will propagate into child makes. Example below.
Also, for the debugging you’re trying to do: there’s an old series
called “Ask Mr Make” (google it) with lots of useful techniques. I
think his article “Tracing Rule Execution”
(http://www.cmcrossroads.com/article/tracing-rule-execution-gnu-make)
might be illuminating about ways to do this without hacking make or
/bin/sh.