On Fri, Apr 20, 2007 at 09:14:43AM +0200, Sascha Wildner wrote: > Petr Janda wrote: > >>You're using the shell builtin. Try /usr/bin/time. :) > >> > >>Sascha > >> > >Thanks, > >Perhaps a note of this could be added the time manual page for people > >like me that didnt know that ;) > > > >Petr > > Hmm, the time(1) manpage does have a reference to builtin(1) (same goes > for echo(1) manpage etc.). > > So _theoretically_ you could have found it. :) >
It's even clearer than that: Some shells may provide a builtin time command which is similar or iden- tical to this utility. Consult the builtin(1) manual page. Petr, What would you suggest to make it clearer? --Peter
pgpCXTVaWrDd0.pgp
Description: PGP signature
