Stream: Coq devs & plugin devs

Topic: Preventing pushing new branches to coq repo

view this post on Zulip Matthieu Sozeau (Dec 07 2020 at 20:14):

I just made the mistake of pushing a branch to coq's repo (now deleted), can't we disallow that?

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 20:49):

Nope, still not possible, though I encourage everyone to complain to https://support.github.com/contact/feedback

view this post on Zulip Gaëtan Gilbert (Dec 07 2020 at 20:50):

can coqbot auto delete them?

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 20:58):

Yes, it can. Should it?

Last updated: Apr 19 2024 at 17:02 UTC