Subject: Re: [bug#41751] [PATCH] gnu: Add bats.
From: Oleg Pykhalov <[email-masked]>
To: [email-masked]
Date: Sat, 25 Jul 2020 22:14:25 +0300
List-Id: <debbugs-submit.debbugs.gnu.org>

All suggestions were applied and pushed in master in
5a88d3dfcb382a9256e5b6d18f1487b597260944.

Closing.