On Thu, 17 Feb 2022, Adam Thornton wrote: > Today I learned that "time" is a shell built-in in zsh! It's been a built-in in a lot of shells for ages; there is also [/usr]/bin/time if you want The Real Thing [tm]. -- Dave