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

[Mark Galeck]

That is great, thank you very much David!  Yes this seems to work so far :)  In 
fact I don't have to use //bin/sh .  I can just do ahead of time
export MAKEFLAGS='SHELL=<different shell than /bin/sh>'


      From: David Boyce <address@hidden>

   
It may still be possible to work around these issues via e.g. the environment.

MAKEFLAGS='SHELL=//bin/sh’ make

This does two things:

1. By putting the setting in the environment it may survive through
intermediate scripts (I thought make did this internally anyway but am
not positive).
2. The extraneous slash in //bin/sh defeats the string match, making a
modification of the binary unnecessary.