Stream: coqbot devs & users

Topic: Merging PR #257

view this post on Zulip Jason Gross (Jan 23 2023 at 19:37):

I'd like to get #257 merged because I have a new PR I want to submit which would conflict with this PR. Last I checked, #257 was working fine. Can I merge it, or can someone review and merge it?

Last updated: May 19 2024 at 16:02 UTC