Delete merged branches from features repository?

[Jean-Marc Lasgouttes]

Le 11/11/2022 à 01:32, Thibaut Cuvelier a écrit :
> On Thu, 10 Nov 2022 at 20:38, Scott Kostyshak <skostysh at lyx.org 
> <mailto:skostysh at lyx.org>> wrote:
> 
>     Should we delete branches from the features repo that have been merged
>     to master? I don't know our policy on this, but it's hard to figure out
>     which branches on the features repo are still relevant (i.e., not yet
>     merged). In the worst case scenario, e.g., where we need to revert the
>     merged branch on master, it is easy to push it again to features.
> 
> 
> +1: it's really a mess, even though it only has like 25 branches.

+1

> It seems it's possible to "hide" a branch while still keeping it around: 
> https://stackoverflow.com/questions/25169440/remove-hide-git-branches-without-deleting-commit-histories 

I am not even sure that we need that, if the branches have been merged. 
Is the information of what branch has been merged lost when the branch 
disappears?

JMarc