Subject: Re: Request for merging "r-team" branch

From: Andreas Enge <[email-masked]>
Date: Mon, 12 May 2025 14:08:40 +0200

Hello Ricardo,

from the number and nature of recent commits on master, I think you have
just merged. Can we close this bug and delete the branch, as suggested
by policy?

How about wip-r-team? It dates from two years ago and is probably
obsolete, but it would be preferable if you could confirm before
deleting it.

Thanks!

Andreas