Re: \timing interval

[ This patch is marked Ready For Committer, and discussion seems to have
died off, so let's get on with committing something ... ]

Corey Huinker <corey.huinker@gmail.com> writes:
> Generally speaking, people disliked the third mode for \timing, and were
> generally fine with AndrewG's idea of printing the timing in both raw
> milliseconds and a more human-digestible format, which means that we can:

Yeah, there seemed to be general agreement on just appending a more human
readable format to the existing printout.

> 3. ignore locales and fall back to a left-trimmed DDD HH:MM:SS.mmm format
>      + Easy to revert to that code
>      + My original format and one PeterE advocated
>      - others disliked

I think this is the approach to go with as a starting point, since it
largely avoids both localization and units-naming concerns.  If someone
feels the desire to build a customizable output format, that can be dealt
with as a separate patch on top of this one ... but I really question that
it'd ever be worth the trouble.

So for clarity's sake: first suitable format among these:

Time: 59.999 ms
Time: 121.999 ms (2:01.999)
Time: 10921.999 ms (3:02:01.999)
Time: 356521.999 ms (4 3:02:01.999)

In an NLS-enabled build, the translator would be able to fool with the
punctuation, though I dunno whether any translators would need to.
        regards, tom lane