[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#67388: 30.0.50; Unintended man page buffer-name change?
|
From: |
Stephen Berman |
|
Subject: |
bug#67388: 30.0.50; Unintended man page buffer-name change? |
|
Date: |
Wed, 29 Nov 2023 18:47:19 +0100 |
|
User-agent: |
Gnus/5.13 (Gnus v5.13) |
On Wed, 29 Nov 2023 18:21:30 +0100 Michael Albinus <michael.albinus@gmx.de>
wrote:
> Stephen Berman <stephen.berman@gmx.net> 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