Re: time

[cjw44@flatline.org.uk (Colin Watson)]

stefan goeman <Stefan.Goeman@siemens.atea.be> wrote:
>I want to use the time command. From the man page I see that there is an option
>+-o (or --output=FILE). However, when I try this, it does not work. In fact, I
>+have the impression that only the -p option is really working. Is this
>a bug or+simply some options that are documented but not implemented
>yet?

'time' also happens to be a bash reserved word, with fewer options: see
'help time' and the "Pipelines" section in 'man bash'. If you want to
use the standalone version described in the man page, invoke it as
'/usr/bin/time'.

(It took me to grab the source for the package, compile it, and wonder
why the freshly compiled binary was working differently to the one I got
by default before I worked out what the problem was, though ...)

-- 
Colin Watson                                     [cjw44@flatline.org.uk]