Subject: Re: bug#67388: 30.0.50; Unintended man page buffer-name change?

From: Stephen Berman <[email-masked]>
Date: Wed, 29 Nov 2023 18:47:19 +0100

On Wed, 29 Nov 2023 18:21:30 +0100 Michael Albinus <[email-masked]> wrote:

> Stephen Berman <[email-masked]> writes:
>
> Hi Stephen,
>
>> Given no reponse in a week, perhaps this fell under the radar, in
>> particular that of Michael Albinus (added to Cc:).
>
> I'm very sorry, I've overlooked this, indeed.
>
>> Michael, if you
>> confirm this was just a typo, I can install the patch to save you the
>> effort.  If it's not a typo, then you're in a better position than me to
>> decide what to do.
>
> Yep, it's a typo. Please install your patch. And thanks for catching this!

Done in commit e87644baa32 on master and closing the bug.  Thanks.

Steve Berman