Show the script's measured running time, not the writer's estimate

The runtime in the header is the sum of the edit_seconds the writer typed,
which is a guess made from a word count. timingHtml renders what the lines
actually take when the cast speaks them, and how far over the target that
puts the trailer - which is the number a revision has to cut to.

trailer.html

@@ -325,6 +325,31 @@
     return out.join("");
   }
 
+  function mmss(n) {
+    return Math.floor(n / 60) + ":" + String(Math.round(n % 60)).padStart(2, "0");
+  }
+
+  // The header's runtime is the sum of what the writer typed. This is what the
+  // lines take when the cast actually says them, which is a different number
+  // and the only one worth cutting against.
+  function timingHtml() {
+    var t = PKG.timing;
+    if (!t || !t.measured_seconds) return "";
+    var over = Number(t.over_by || 0);
+    var line = "Spoken by the cast this script runs <b>" + mmss(t.measured_seconds)
+      + "</b>, against a " + mmss(t.target_seconds) + " target";
+    if (over > 5) line += " — <b>" + Math.round(over) + " seconds over</b>."
+      + " Revising the whole script will cut that much.";
+    else if (over < -15) line += " — " + Math.round(-over) + " seconds short.";
+    else line += " — that fits.";
+    var worst = (t.longest_lines || []).slice(0, 3).map(function (l) {
+      return "<li>" + Number(l.seconds || 0).toFixed(1) + "s &middot; shot "
+        + esc(String(l.shot)) + " &middot; “"
+        + esc(String(l.text || "").slice(0, 80)) + "”</li>"; }).join("");
+    return '<div class="timing' + (over > 5 ? " over" : "") + '"><div>' + line + "</div>"
+      + (worst && over > 5 ? "<ul>" + worst + "</ul>" : "") + "</div>";
+  }
+
   function reviewsHtml(meta) {
     var mine = REVIEWS.filter(function (r) {
       return r.subject === meta.writer && Number(r.iteration) === Number(meta.iteration); });