Eric Blake wrote:
Re-adding the list - I am not the bash maintainer, so keeping the list in
the loop is essential if you want any action taken.
I am the bash maintainer, so I figure my opinion will count for something.
| So there's a bug in the manual, which does not breathe a word about
| time being executed by the shell. And the shell covers its tracks, too:
I think the manual's pretty clear about where and how time is implemented.
It's just not mentioned in the builtins section, since:
|
| % builtin time
| bash: builtin: time: not a shell builtin
it's not a builtin.
|
| Were I still the keeper of Unix manuals, my fix to the manual
| would be to list this wart under BUGS.
Ummm...why, exactly? The manual accurately describes the implementation,
which conforms to the relevant standards.
A Posix implementation may provide another version of time as a separate
utility, which will accommodate your desired usage. Even something like
#! /bin/sh
time "$@"
would suffice and allow builtins, if not pipelines, to be timed.
Chet
--
``The lyf so short, the craft so long to lerne.'' - Chaucer
Live Strong. No day but today.
Chet Ramey, ITS, CWRU [EMAIL PROTECTED] http://cnswww.cns.cwru.edu/~chet/
