[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: how to use a different /bin/sh with GNU Make?
From: |
Mark Galeck |
Subject: |
Re: how to use a different /bin/sh with GNU Make? |
Date: |
Thu, 15 Oct 2015 20:23:45 +0000 (UTC) |
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.