On Wed, Nov 09, 2005 at 03:23:13PM +0100, Geert Hendrickx wrote: > On Wed, Nov 09, 2005 at 02:59:53PM +0100, Joris van der Hoeven wrote: > > This issue is indeed a bit problematic, because some systems don't have > > /bin/bash, while others don't use bash as the standard shell. In the > > past, I changed from /bin/sh to /bin/bash because several people asked me > > to do so. Now you ask me to go the other way around. What would be a > > more reasonable solution? > > > > Best wishes, Joris > > Since you don't use any bash extensions, it works with any POSIX /bin/sh > (including bash), so #!/bin/sh is really the most appropriate here.
I am not sure that we don't use any bash extensions somewhere. > 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... Best, Joris _______________________________________________ Texmacs-dev mailing list [email protected] http://lists.gnu.org/mailman/listinfo/texmacs-dev
