@Théo Zimmermann , the v8.17 branch is created, I understand that you'd prefer the v8.17 to be in sync with the backports PR CI?
If so I can indeed do that, I agree that https://github.com/coq/coq/pull/16944 has not a lot of motivation to be in 8.17 IMO
Yes, I got the milestone wrong, and I just removed it
There is also no argument against having it in 8.17 tho, so as the RM prefers, for now I've made it 8.18-only on SerAPI but Théo ping me and I'll add it back.
My policy is to avoid backporting PRs with overlay as much as possible.
Last updated: Jun 11 2023 at 01:30 UTC