Subject: Re: [PATCH] gnu: mercury: Use #:select instead of comment string.

From: Raghav Gururajan <[email-masked]>
Date: Wed, 27 Apr 2022 22:41:15 -0400

Pushed as f1d08be7af to master. Thanks for the patch.

Regards,
RG.