Noah Misch <noah(at)leadboat(dot)com> writes:
> On Sun, Jul 22, 2018 at 10:46:03AM -0400, Tom Lane wrote:
>> The pg_upgrade makefile does in fact use $(SHELL), so it will default to
>> whatever shell configure used.
> It will not, because we don't set $(SHELL) anywhere. $(SHELL) is not @SHELL(at)(dot)
> In our makefiles, $(SHELL) is always /bin/sh, the GNU make default.
Oh! Hm, I wonder whether we shouldn't do that, ie add SHELL = @SHELL@
to Makefile.global.in.
A quick trawl of the buildfarm logs says most of our animals compute
SHELL = /bin/sh anyway, and so would be unaffected. There's a sizable
population that find /bin/bash though, and one active critter that finds
/bin/ksh.
regards, tom lane