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Â
	echo bar
/tmp/foo $ SHELL=/bin/true make test
echo bar
/tmp/foo $ make test SHELL=/bin/true
echo bar

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


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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