bug#65251: 30.0.50; Duration in compilation buffer

[Mattias Engdegård]

17 aug. 2023 kl. 20.48 skrev Helmut Eller <eller.helmut@gmail.com>:

> Here it is:

Thank you! Pushed to master with some very slight editing, under my own name 
(but your credit) since you seemed reluctant about the changes -- hope that is 
all right.

(I think we prefer patches as attachments -- I had to edit it a bit to apply, 
which wasn't any trouble since the patch was so short.)

Further improvements are perfectly possible, but this is unquestionably an 
improvement.
Otherwise, if you aren't too unhappy about the resolution, the bug can be 
closed.