[wfleming]

You could use something like `sh -c 'time ...'` to work around that. (You might need bash instead of sh, it might depend on what sh is on your system.)

[efortis]

Thank you, that worked well. I added it to the post.