Moritz Schulte <[EMAIL PROTECTED]> wrote: >stefan goeman <[EMAIL PROTECTED]> 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 [EMAIL PROTECTED]
