Re: [isabelle] Isabelleâs getsettings somehow broken



Hi Florian,

Am Mittwoch, den 17.02.2016, 09:35 +0100 schrieb Florian Haftmann:
> E.g. make does interpret SHELL that way;

that is actually not the case:

/tmp/foo $ cat MakefileÂ
test:
	echo bar
/tmp/foo $ SHELL=/bin/true make test
echo bar
bar
/tmp/foo $ make test SHELL=/bin/true
echo bar

it seems you confused makeâs Makefile variable SHELL with the
environment variable SHELL.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.