[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: |
Tue, 13 Oct 2015 10:00:06 +0000 (UTC) |
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.