Date: Sat, 15 Jul 2017 17:23:18 +0200
From: "rudolf%eq.cz@localhost" <rudolf%eq.cz@localhost>
Message-ID: <607b1fb2-37d9-0f39-c19e-26090c43e7f2%eq.cz@localhost>
| The "times" command is not currently documented in the sh man page.
Ugh, you're correct - one more thing to fix...
kre