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