On Sun, 2009-04-26 at 13:44 +0200, Joris van der Hoeven wrote: > I am surprised by the problem under Ubuntu: is /bin/sh not there? > This is weird, since UNIX requires /bin/sh to exist.
On Ubuntu, /bin/sh is the dash shell. http://en.wikipedia.org/wiki/Debian_Almquist_shell The dash shell is much smaller and significantly faster than bash. _______________________________________________ Texmacs-dev mailing list [email protected] http://lists.gnu.org/mailman/listinfo/texmacs-dev
