Re: [isabelle] Isabelleâs getsettings somehow broken


Am Donnerstag, den 11.02.2016, 09:25 +0100 schrieb Florian Haftmann:
> > 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.

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.