4 May
2020
4 May
'20
5:24 p.m.
Dmitry Baryshkov dbaryshkov@gmail.com writes:
I just wanted to point that git tree was not updated for the release.
Thanks for telling me! Should be up to date now.
I think the way it happened, was that I ran git push --tags under the assumption that it would push tags in addition to the current branch, and I didn't pay close attention.
Regards, /Niels
--
Niels Möller. PGP-encrypted email is preferred. Keyid 368C6677.
Internet email is subject to wholesale government surveillance.