bug#65251: 30.0.50; Duration in compilation buffer

[Eli Zaretskii]

> From: Helmut Eller <eller.helmut@gmail.com>
> Cc: mattias.engdegard@gmail.com,  65251@debbugs.gnu.org
> Date: Thu, 17 Aug 2023 07:55:37 +0200
> 
> On Thu, Aug 17 2023, Eli Zaretskii wrote:
> 
> > It sounds like you reject all of Mattias's comments?  That's somewhat
> > unusual around here.  Does that above mean that you insist on
> > submitting your original patch with no further changes, or will you be
> > sending an updated patch?
> 
> I can submit an updated patch, if it is wanted.  But it didn't sound
> like that me.  I can also continue using compilation-finish-functions in
> my .emacs, if that's easier for you.

I intended to install this once there are no more review comments, as
I think this could be a useful addition.  I believe Mattias also
thought the idea was a good one.  So my preference is for you to post
an updated patch, yes.

TIA