Subject: Re: [PATCH] gnu: mercury: Use #:select instead of comment string.
From: Raghav Gururajan <[email-masked]>
To: [email-masked]
Cc: jgart <[email-masked]>
Date: Wed, 27 Apr 2022 22:41:15 -0400
List-Id: <debbugs-submit.debbugs.gnu.org>

Pushed as f1d08be7af to master. Thanks for the patch.

Regards,
RG.