13 Jan
2009
13 Jan
'09
6:24 p.m.
Jeff wrote:
Unless somebody else can shed some more light on this, I guess you are stuck with output redirection provided by your chosen shell.
Try /usr/bin/time instead of 'time', I believe 'time' is a internal command for bash as well.
Threw me off for a while as well. (e.g. redirecting time output to a file does not work unless you call /usr/bin/time, even redirecting stderr, at least last time I tried)
nate