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