Changes by: Aleksey Nogin (nogin at metaprl.org)
Date: 2007-07-02 12:12:29 -0700 (Mon, 02 Jul 2007)
Revision: 11189
Log message:

      Added Omake_util.pp_time that would print the time as
     "%0.2f sec", or
     "%d min %05.2f sec", or
     "%d hrs %02d min %05.2f sec"
     depending on how big it is. This follows Sam's (sds at gnu.org) suggestion
     from bug #680.