Subject: Re: bug#56507: Suggestions for the "Options" menu
From: Stefan Kangas <[email-masked]>
To: Lars Ingebrigtsen <[email-masked]>
Cc: [email-masked]
Date: Tue, 12 Jul 2022 09:38:45 -0500
List-Id: <debbugs-submit.debbugs.gnu.org>

Lars Ingebrigtsen <[email-masked]> writes:

> I think I prefer to keep those options as is.

I guess we won't make more progress here so I'm closing the bug.
Thanks for considering my suggestions.