On 4. Jul 2019, at 01:41, Pau Espin Pedrol
<pespin(a)sysmocom.de> 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