I'd really like to see this feature happen. @Théo Zimmermann do you have any updates on https://github.com/coq/bot/issues/107 ? Is there anything I can do to make this happen sooner?
Really sorry about that @Jason Gross. I've been completely overwhelmed, so I couldn't even take time to answer your last comment. I'll make sure to do it soon.
Cool, thanks, and thanks for the response here, and no worries. Good luck with whatever's overwhelming you!
Last updated: Jan 31 2023 at 09:01 UTC