Stream: Coq devs & plugin devs

Topic: requesting assignee

view this post on Zulip Gaëtan Gilbert (May 21 2021 at 10:55):

https://github.com/coq/coq/pull/14238

view this post on Zulip Pierre-Marie Pédrot (May 21 2021 at 10:56):

I could assign but I don't understand anything to the notification code

view this post on Zulip Pierre-Marie Pédrot (May 21 2021 at 10:57):

(not that it matters a lot, but I want to highlight it before I get complaints)

view this post on Zulip Gaëtan Gilbert (May 21 2021 at 11:38):

that pr has nothing to do wth notifications

view this post on Zulip Pierre-Marie Pédrot (May 21 2021 at 11:54):

whatever you call that, I mean sending HTTP requests to Zulip

view this post on Zulip Pierre-Marie Pédrot (May 21 2021 at 11:54):

Ah, sorry, mixed that with the other PR...

Last updated: May 31 2023 at 15:01 UTC