Re: [isabelle] Isabelleʼs getsettings somehow broken



On Wed, 10 Feb 2016, Joachim Breitner wrote:

One way out might be to follow the advice that I procured here: http://stackoverflow.com/a/35324612/946226 This way, you can avoid the call to /bin/sh in the problematic part src/Pure/Concurrent/bash.ML. Iâm not sure if this is available on Windows.

In the last 10 years I have rewritten equivalents of OS.Process.system on ML and JVM several times, for all platforms. In Isabelle2016 we have native Windows for Poly/ML, which gives more liberty next time -- if and when SML/NJ is also discontinued. I once had a plain Unix fork/exec in ML with /bin/bash that never went into the repository, because it was not portable enough.

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.


Right now I am trying to get a feel about the actual impact of /bin/sh -> /bin/dash in Linux distributions apart from Debian + Ubuntu.

How fast will Debian-testing move forward towards production releases? So far my stable Ubuntu 15.10 looks still fine.


	Makarius


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