Subject: Request for merging "r-team" branch
From: Ricardo Wurmus <[email-masked]>
To: [email-masked]
Date: Wed, 17 Jul 2024 23:23:33 +0200
List-Id: <debbugs-submit.debbugs.gnu.org>

The branch has been merged with commit
7ccd8ade8b17897281bb6793acf121a88a1137e3.

-- 
Ricardo