Re: redirect time to file

[Erik Xavior]

wow. Thank you!!

and can I append the output of "time" to a file? [like "time echo hi >>
file"]

eg.: it could be good, for measuring a commands running time several times,
then avg the "time"'s output!! :D :O