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

[Andrea Gamba]

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.

Andrea