Joris van der Hoeven wrote: >I am not sure that we don't use any bash extensions somewhere. > > On Debian/Ubuntu, one nice way to check this, is to install 'dash' as the /bin/sh. It is a slim POSIX-compliant shell that may even speed up scripts.
>>Why did they ask you to change it to /bin/bash? >> >> > >Because it did not work on some systems. I will have to dig up my email for >this; >you may search the mailing list archives too... > > This would be very interesting. I guess, the scripts would simply use some bashianism. Changing the headline is the cheap way out, but for portability, the scripts should really run with /bin/sh _______________________________________________ Texmacs-dev mailing list [email protected] http://lists.gnu.org/mailman/listinfo/texmacs-dev
