Hello plugin authors, apparently some shell-scripts depend on bash but use #!/bin/sh. This causes problems with distros that do not use bash as default shell, see
https://savannah.gnu.org/bugs/index.php?18519 Ideally, everyone whose script uses bash specific features would change the first line to #!/bin/bash. As not everyone is going to read this mail, and as bash is included in (virtually ?) all desktop distros, I suggest we proceed the other way around: we switch all #!/bin/sh shell scripts to #!/bin/bash unless someone knows for sure that a given script does not use bash specific features. Comments? Vetoes? Thanks, Felix _______________________________________________ Texmacs-dev mailing list [email protected] http://lists.gnu.org/mailman/listinfo/texmacs-dev
