GitHub webhook has been successfully configured by Zimmi48.
ppedrot opened PR #1 Port to 8.15 from
This is a cleanup that makes this contribution compile with 8.15.
First time this webhook is triggered :surprise:
I think the huge army of coq-contrib contributors-to-be were just waiting for this moment (for someone to open a new PR before they do)
Looks like we are left in a bit of a dilemma here what will happen to these changes:
I volunteered for this patch and stepped down immediately...
The project should stay in coq-contribs then. We could ask Hugo to look at the PR or Pierre-Marie could just merge the PR himself since he has the rights to do so.
yes, if you don't mind I will ask him to merge
ppedrot merged PR #1 Port to 8.15.
brando90 opened issue #5 for what coq versions does this work?
Last updated: Feb 05 2023 at 14:02 UTC