Subject: Re: [bug#37239] [PATCH] gnu: mariadb: Split into out, lib and dev.
From: Julien Lepiller <[email-masked]>
To: [email-masked]
Date: Sat, 12 Oct 2019 13:08:55 +0200
List-Id: <debbugs-submit.debbugs.gnu.org>

Pushed as 2b8491fbbe818944baf454faf1326034022ac320 on staging. Thank
you!