bug in time?

[Luciano Miguel Ferreira Rocha]

On Sat, Feb 07, 2004 at 06:45:12PM -0500, Christopher K. Johnson wrote:
> Luciano Miguel Ferreira Rocha wrote:
> 
> >On Sat, Feb 07, 2004 at 11:41:44PM +0200, m l wrote:
> >Bash uses its own internal time command, so it gives an error when you 
> >don't
> >pass the comand to be executed to time.
> >
> >You can get bash's time help with:
> >1. man bash
> >2. help time
> >
> >System's time is also available by specifying its full path:
> >/usr/bin/time cmd
> >
> >Regards,
> >Luciano Rocha
> >
> >
> > 
> >
> Actually csh has an internal command for time.  Bash doesn't and 
> consequently uses the time command found via the path.

No, bash has its own time command. But not a which command, that's why
which doesn't know about bash's time.

>From bash's manual page:
    If the time reserved word precedes a pipeline, the elapsed as  well as
    user  and  system  time consumed by its execution are reported when the
    pipeline terminates.  The -p option changes the output format  to  that
    specified  by  POSIX.   The  TIMEFORMAT variable may be set to a format
    string that specifies how the timing information should  be  displayed;
    see the description of TIMEFORMAT under Shell Variables below.

Regards,
Luciano Rocha