Subject: Request for merging "r-team" branch

From: Ricardo Wurmus <[email-masked]>
Date: Wed, 17 Jul 2024 23:23:33 +0200

The branch has been merged with commit
7ccd8ade8b17897281bb6793acf121a88a1137e3.

-- 
Ricardo