lib/scripts/timestop.bash
2015-08-20 wenzelm 2015-08-20 suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
2009-05-31 wenzelm 2009-05-31 uniform treatment of shellscript mode;
2008-12-20 wenzelm 2008-12-20 removed Ids;
2008-10-03 wenzelm 2008-10-03 factor: proper padding of digits;
2008-10-02 wenzelm 2008-10-02 time factor: one more digit;
2008-10-02 wenzelm 2008-10-02 include factor in timing report;
2005-12-01 wenzelm 2005-12-01 cpu time = user + system;
2005-12-01 wenzelm 2005-12-01 timestop - report timing based on environment (cf. timestart.bash);