> On 4. Jul 2019, at 01:41, Pau Espin Pedrol <[email protected]> wrote:
>
> Hi Holger,
>
> So, I want to ask if there's some explanation for those tags missing or you
> simply forgot to push them when creating the releases (or they got somehow
> lost in the server).
>
> Do you happen to have the tags locally and can push them? or otherwise
> generate the tags now and push them. I can also do it if you want, I'll push
> tags on the commits from the list I wrote above.
I don't have them locally either. Feel free to add them retro-actively.
holger
