On Mon, Apr 27, 2009 at 11:38:28AM +0200, David Allouche wrote: > 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.
Thanks, --Joris Those who experienced problems with the plug-ins, can you give more precisions about what goes wrong? _______________________________________________ Texmacs-dev mailing list [email protected] http://lists.gnu.org/mailman/listinfo/texmacs-dev
