On Thu, Aug 8, 2024, 8:13 AM Greg Wooledge <g...@wooledge.org> wrote:
> On Thu, Aug 08, 2024 at 15:08:33 +0200, Franco Martelli wrote: > > The Bash's shell keyword "time" it could be fine, but I don't know how to > > redirect its output to a file (-o switch of /usr/bin/time). > > https://mywiki.wooledge.org/BashFAQ/032 The Bash FAQ has always amazed me with articles like that. And then I wonder how many lives might depend on the minutiae of "time" vs. /usr/bin/time or some equally involved (dare I say "arcane"?) detail of bash scripting.... And then I feel tired :-)
