Re: \timing interval

<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Sep 1, 2016 at 2:17 PM, Tom Lane <span
dir="ltr"><<ahref="mailto:tgl@sss.pgh.pa.us" target="_blank">tgl@sss.pgh.pa.us</a>></span> wrote:<br
/><blockquoteclass="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">I
wrote:<br/> > So for clarity's sake: first suitable format among these:<br /><br /> > Time: 59.999 ms<br /> >
Time:121.999 ms (2:01.999)<br /> > Time: 10921.999 ms (3:02:01.999)<br /> > Time: 356521.999 ms (4
3:02:01.999)<br/><br /></span>Sorry, that probably added no clarity at all, I was confusing<br /> seconds with
millisecondsin the example values :-(<br /><br />                         regards, tom lane<br /></blockquote></div><br
/>Ididn't scan your examples for correctness, but the parentheticals matched my own idea for what "left-trimmed"
meant.</div><divclass="gmail_extra"><br /></div><div class="gmail_extra">I'm going to hold off a bit to see if anybody
elsechimes in, and if not I'm going to deliver a patch.<br /><br /></div></div>