time command with shell builtins

[Dominik Vogt <dominik.vogt@xxxxxx>]

The "time" command does not seem to work with builtin commands:

  $ which time
  time: shell reserved word

  # works
  $ time /bin/echo
  /bin/echo  0.00s user 0.00s system 61% cpu 0.002 total

  # doesn't work
  $ time echo
  # no output

Is it possible to get timing statistics of shell builtins too?
Timing "echo" isn't very interesting, but timing loop constructs
would be:

  $ time while foo; do bar done

Ciao

Dominik ^_^  ^_^

--

Dominik Vogt