"brian m. carlson" <[EMAIL PROTECTED]> 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 PROTECTED]> 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. -- Ben Pfaff http://benpfaff.org -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
