Re: [isabelle] Isabelleʼs getsettings somehow broken



On Wed, 10 Feb 2016, Gerwin Klein wrote:

Weʼve just had the exact same problem yesterday on 2016-RC4 + Ubuntu. Not sure what the resolution was, let me find out.

I am definitely interested in that. So far my impression is that only Debian-testing has that dangerous version of dash-0.5.8, see also https://tracker.debian.org/news/744916

The longer I think about it, the less I like it: on a system where with /bin/sh -> dash the "export -f" feature of bash is effectively destroyed, since /bin/sh -c happen in many tools and libraries.


	Makarius


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