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
_______________________________________________
Texmacs-dev mailing list
[email protected]
http://lists.gnu.org/mailman/listinfo/texmacs-dev
