Peter Avalos wrote:
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
Perhaps I should read more carefuly :)
Petr
