Hi, Greg Wooledge wrote: > > > * TIMEFORMAT=... time foo will invoke /usr/bin/time, but > > > TIMEFORMAT=... eval time foo will use the builtin.
I wrote: > > I wonder about the formal reason for this. > There are some mysteries in bash that I'm content simply to write off as > "here be magic". At least i know by now why i got to see two output formats of "time" during the last 30 years of GNU/Linux programming If not for the tangible help, i cherrish this list for the background information which floats along here. Have a nice day :) Thomas