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.
Why did they ask you to change it to /bin/bash?
Geert
_______________________________________________
Texmacs-dev mailing list
[email protected]
http://lists.gnu.org/mailman/listinfo/texmacs-dev
