Re: [isabelle] Isabelleʼs getsettings somehow broken
On Wed, 10 Feb 2016, Makarius wrote:
I have already studied the openjdk-8 sources, and it seems that it does
*not* use /bin/sh under normal circumstances -- that is only a
fall-back. So patching Poly/ML could work, but anybody doing plain Unix
programming with "system" functions (e.g. in perl) will fall again on
his nose with a bad /bin/sh.
I have done this now in
evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably
on Ubuntu and Debian)
Moreover, there was one perl "system" invocation to be replaced in the
invoke perl system with explicit list -- to avoid extra /bin/sh and thus
evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu
In common street language that would probably called a "fix", but it is
just careful avoidance of something that is documented in the bash man
page (export -f) and no longer works on Debian-testing. The problem is not
solved, merely its consequences are hidden.
From the Isabelle side we can hopefully proceed towards the release: there
needs to be a re-spin and another release candidate (probably tomorrow),
and people on isabelle-users will have to make one more round of testing
-- extremely few have done this so far.
This archive was generated by a fusion of
Pipermail (Mailman edition) and