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 <d...@boyski.com>
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.
_______________________________________________
Help-make mailing list
Help-make@gnu.org
https://lists.gnu.org/mailman/listinfo/help-make
