+1 on solving the general problem of "I forgot to set \timing--how
long did this run?". I could have used that more than once in the
past, and I'm sure it will come up again.
I think Heikki's solution is probably more practical since (1) even if
we add the prompt parameter originally proposed, I don't see it being
included in the default, so it would require users to change their
prompt before they can benefit from it and (2) even if we commit to
never allowing tweaks to the format, I foresee a slow but endless
trickle of requests and patches to do so.
Thanks,
Maciek
