Re: [Texmacs-dev] /bin/sh vs. /bin/bash in Ubuntu

[Joris van der Hoeven]

On Mon, Apr 27, 2009 at 09:26:31PM +0200, Andrea Gamba wrote:
> Andrey G. Grozin wrote:
> >
> >I don't know what other bash-specific features are used in these 
> >scripts. Probably, there are some, because there is some breakage on 
> >ubuntu. Ubuntu users can investigate what scripts (and what lines in 
> >them) don't work in the expected way.
> >
> This is a third possible solution: to fix the plugins one-by-one for 
> compatibility with dash. It is going to take some time however. And if a 
> solution is not found for some plugin, I think that the /bin/sh -> 
> /bin/bash change should be considered as a compromise.

This compromise is known to fail on several architectures,
so it is best to make our scripts "all-shell-compatible".
What exactly do we use which is not supported by dash?

Best wishes, Joris