Re: time

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

Moritz Schulte <tux@gmx.li> wrote:
>stefan goeman <Stefan.Goeman@siemens.atea.be> writes:
>> 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?
>
>There is a program '/usr/bin/time' and there's a Bash builtin
>'time'.

Note that it's not quite a bash builtin as such; if it were a builtin,
then 'enable -n time' would work ...

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