Re: \timing interval

I wrote:
> Attached is an updated patch that does it like that.  Sample output
> (generated by forcing specific arguments to PrintTiming):

> Time: 0.100 ms
> Time: 1.200 ms
> Time: 1001.200 ms (00:01.001)
> Time: 12001.200 ms (00:12.001)
> Time: 60001.200 ms (01:00.001)
> Time: 720001.200 ms (12:00.001)
> Time: 3660001.200 ms (01: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: 8816460001.200 ms (102 01:01:00.001)
> Time: 8856720001.200 ms (102 12:12:00.001)

After further thought I concluded that not providing any labeling of
days is a bad idea.  The hours, minutes, and seconds fields seem
reasonably self-explanatory given the formatting, but days not so much.
(I'm not sure whether that is the whole of Peter van H's objection,
but surely it's part of it.)  I pushed the patch using this:

Time: 176460001.200 ms (2 d 01:01:00.001)

and all else as before.
        regards, tom lane