Re: [isabelle] Isabelleâs getsettings somehow broken



>>> An alternative is to modify Poly/ML to use /bin/bash or
>>> getenv(SHELL)
>>> instead of hardwired /bin/sh -- that would be a typical Debianistic
>>> patch.
>>
>> getenv(SHELL), falling back on /bin/sh by default is a very custom
>> behaviour and would make sense; nevertheless the user still has the
>> burden of setting SHELL explicitly in case of problems.
> 
> is it? Isnât "SHELL" how a user configures his preferred _interactive_
> shell? That might be ksh, or fish, or even ghci for all you know...
> Likely not something you want to rely on.

E.g. make does interpret SHELL that way;  but that seems indeed not to
be representative:

> haftmann at scarlatti:/data$ SHELL=/usr/bin/tclsh python -c 'import os; os.system("ps -f")'
> UID        PID  PPID  C STIME TTY          TIME CMD
> haftmann  3286  3030  0 08:46 pts/0    00:00:00 bash
> haftmann  5800  3286  0 09:33 pts/0    00:00:00 python -c import os; os.system("ps -f")
> haftmann  5801  5800  0 09:33 pts/0    00:00:00 sh -c ps -f
> haftmann  5802  5801  0 09:33 pts/0    00:00:00 ps -f

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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