GitLab subgroups fix for #120 still needs some finalisation

Open myii opened this issue 5 years ago • 0 comments

#120 has been fixed but there are still a couple of outstanding problems to be resolved, as based on this discussion with @Zimmi48 in Zulip:

https://coq.zulipchat.com/#narrow/stream/243318-coqbot-devs.20.26.20users/topic/How.20to.20troubleshoot.20coqbot.3F/near/220304637

If I understand the discussion correctly, this may be resolved when this fix is made:

Dec 18 '20 17:12 myii