Eli Zaretskii writes: >> From: Philip Kaludercic >> Cc: larsi@gnus.org, 55039@debbugs.gnu.org >> Date: Wed, 07 Sep 2022 18:27:18 +0000 >> >> Eli Zaretskii writes: >> >> >> I've just remove the changes to the manual from my patch. >> > >> > Why? That was nowhere near what I intended to say with the above >> > comments, which were minor. >> >> It wasn't because of your comments, rather I just felt mentioning it was >> too clumsy, and a few others said they didn't feel it was necessary to >> mention the option in the manual. But if you think that it should be >> added, then I'll try it again and take your comments into account. > > Yes, I think it should be in the manual. But if you'd rather leave > that to me, I'm fine with that. Here is my latest attempt (will merge it into the patch):