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