Subject: Done
From: Brian Leung <[email-masked]>
To: [email-masked], [email-masked]
Date: Thu, 10 Oct 2019 18:03:53 +0200
List-Id: <debbugs-submit.debbugs.gnu.org>

Thanks for the patch. I made some small changes and merged.