[Texmacs-dev] plugins depend on bash but use #!/bin/sh

[Felix Breuer]

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