Re: \timing interval

I wrote:
> Sorry, that probably added no clarity at all, I was confusing
> seconds with milliseconds in the example values :-(

After a bit of further fooling with sample values, I propose this
progression:

Time: 0.100 ms
Time: 1.200 ms
Time: 1001.200 ms (0:01.001)
Time: 12001.200 ms (0:12.001)
Time: 60001.200 ms (1:00.001)
Time: 720001.200 ms (12:00.001)
Time: 3660001.200 ms (1:01:00.001)
Time: 43920001.200 ms (12:12:00.001)
Time: 176460001.200 ms (2 01:01:00.001)
Time: 216720001.200 ms (2 12:12:00.001)
Time: 10000000000000000000.000 ms (115740740740 17:46:40.000)

Note that times from 1 second to 1 hour all get the nn:nn.nnn
treatment.  I experimented with these variants for sub-minute times:

Time: 1001.200 ms (1.001)
Time: 12001.200 ms (12.001)
Time: 1001.200 ms (1.001 s)
Time: 12001.200 ms (12.001 s)

but it seems like the first variant is not terribly intelligible and
the second variant is inconsistent with what happens for longer times.
Adding a zero minutes field is a subtler way of cueing the reader that
it's mm:ss.
        regards, tom lane