Re: \timing interval

<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Sep 1, 2016 at 3:01 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="">CoreyHuinker <<a href="mailto:corey.huinker@gmail.com">corey.huinker@gmail.com</a>> writes:<br /> >
OnThu, Sep 1, 2016 at 2:43 PM, Tom Lane <<a href="mailto:tgl@sss.pgh.pa.us">tgl@sss.pgh.pa.us</a>> wrote:<br
/></span><spanclass="">>> Note that times from 1 second to 1 hour all get the nn:nn.nnn<br /> >>
treatment. I experimented with these variants for sub-minute times:<br /></span>>> ...<br /><span
class="">>>but it seems like the first variant is not terribly intelligible and<br /> >> the second variant
isinconsistent with what happens for longer times.<br /><br /></span><span class="">> Well, if we're looking to be
consistent,here's what interval does now:<br /></span>> ...<br /><span class="">> Should we just plug into
whatevercode that uses?<br /><br /></span>Well, that code's on the backend side so we're not going to just call it<br
/>in any case.  And I think we don't want to be quite so verbose as to go up<br /> to hh:mm:ss.fff as soon as we get
past1 second.  However, comparing that<br /> output to what I had suggests that maybe it's better to keep a leading<br
/>zero in two-digit fields, that is render times like "00:01.234",<br /> "01:23.456", or "01:23:45.678" rather than
suppressingthe initial zero as<br /> I had in my examples.  It's an extra character but I think it reinforces<br /> the
meaning.<br/><br />                         regards, tom lane<br /></blockquote></div><br /></div><div
class="gmail_extra">+1</div><divclass="gmail_extra">The larger jump in widths from no MM:SS to HH:MM:SS is a good
visualcue. Jumping from MM:SS to H:MM:SS to HH:MM:SS would be more subtle and possibly confusing.</div><div
class="gmail_extra"><br/></div><div class="gmail_extra"><br /></div><div class="gmail_extra"><br /></div></div>