"brian m. carlson" <firstname.lastname@example.org> writes:
> On Fri, Dec 07, 2007 at 04:51:29AM +1000, Anthony Towns wrote:
>>On Thu, Dec 06, 2007 at 07:42:06AM -0800, Russ Allbery wrote:
>>> Anthony Towns <email@example.com> writes:
>>> > time (???)
>>> Likewise. time is a standard Unix program.
>>And which is a built-in on bash, tcsh and zsh, so doesn't seem terribly
>>useful most of the time... (not dash though)
> I've never seen anyone use either dash or posh as their default shell,
> and IME time is only used in interactive shells, so this might not be
> that important. IMHO it could be relegated to optional.
I use "time" in benchmarking scripts.