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: Jun 04 2023 at 23:30 UTC