Hi,
On Tue, Jan 13, 2009 at 13:24, nate centos@linuxpowered.net wrote:
Try /usr/bin/time instead of 'time', I believe 'time' is a internal command for bash as well.
Right.
However, /usr/bin/time won't accept the syntax above, this will not work: $ /usr/bin/time { date; }
Of course you can: $ /usr/bin/time date
Or: $ /usr/bin/time sh -c '{ date; }'
Or: $ /usr/bin/time bash -c '{ date; }'
If you want to use the external binary instead of the built-in, but you don't want to type the full path, you can use the trick to add a backslash in front of the command name: $ \time -o file date
If you want to use the built-in "time" available in bash, you can get a reference to its options with the command: $ help time
You will see that the only option it supports is -p to slightly change the format, but not -o for the output. You should do redirection with
and/or 2> to write to a file.
Another advantage of the built-in is that it does time a full pipeline. For example, this will time both date and grep: $ time date | grep Sat
While this will time date only: $ /usr/bin/time date | grep Sat
HTH, Filipe