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 "mirabelle" tool:

  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 MHonArc.