lib/scripts/timestop.bash
Thu, 01 Dec 2005 18:44:47 +0100 wenzelm cpu time = user + system;
Thu, 01 Dec 2005 18:37:39 +0100 wenzelm timestop - report timing based on environment (cf. timestart.bash);
less more (0) tip