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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and