Subject: Re: [bug#62886] Unnecessary bug registered

From: Karl Berry <[email-masked]>
Date: Sat, 27 May 2023 19:22:04 -0600

Closing bug as suggested. Mailing or cc-ing [email-masked]
will close a bug.

    To be closed/deleted, just like 
    https://debbugs.gnu.org/cgi/bugreport.cgi?bug=60419.

Merging that one. --thanks, karl.