16 Mar
2022
16 Mar
'22
6:58 p.m.
Daniel-Constantin Mierla writes:
Just noticed that the previous git push failed for
what so ever reason
-- I did it again and now the commit should be in the repo.
Thanks, now sanity_check() detects the empty user part. It is possible
to backport this?
-- Juha