Subject: Close

From: Andreas Enge <[email-masked]>
Date: Wed, 4 Dec 2024 11:54:57 +0100

This has been merged, closing the bug.

I would suggest to also delete the branch, as this makes clear which
branches are currently active, but my impression is that different teams
handle this differently, so I will not go ahead.

Andreas