bug#56155: 29.0.50; Options menu, toggle menu items not updated

[Gerd Möllmann]

Lars Ingebrigtsen <larsi@gnus.org> writes:

> Gerd Möllmann <gerd.moellmann@gmail.com> writes:
>
>> I think the bug can be closed, but I don't see how I could do that.
>> Or maybe I can't and shouldn't, I don't know.
>
> You can close the bug by sending a mail to 56155-close@debbugs.gnu.org,
> but there still seems to be discussions about more general ways to fix
> this...

Nothing seems have come out the discussions, so I'm closing this.