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