title: Custom format for time command
body: <p>I'd like to use the <strong>time</strong> command in a <strong>bash script</strong> to calculate the elapsed time of the script and write that to a log file.  I only need the <strong>real time</strong>, not the user and sys.  Also need it in a decent format. e.g 00:00:00:00 (not like the standard output).  I appreciate any advice.</p>
  
  <p>The expected format supposed to be <code>00:00:00.0000</code> (milliseconds) [hours]:[minutes]:[seconds].[milliseconds]</p>
  
  <p>I've already 3 scripts. I saw an example like this:</p>
  
  <pre><code>{ time { # section code goes here } } 2&gt; timing.log
  </code></pre>
  
  <p>But I only need the real time, not the user and sys. Also need it in a decent format. e.g <code>00:00:00:00</code> (not like the standard output).</p>
  
  <p>In other words, I'd like to know how to turn the time output into something easier to process.</p>