Emilio Jesús Gallego Arias (Dec 15 2022 at 10:40): Emilio Jesús Gallego Arias (Dec 15 2022 at 10:40):@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?
Emilio Jesús Gallego Arias (Dec 15 2022 at 10:41):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
Enrico Tassi (Dec 15 2022 at 10:52):Yes, I got the milestone wrong, and I just removed it
Emilio Jesús Gallego Arias (Dec 15 2022 at 11:10):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.
Théo Zimmermann (Dec 15 2022 at 14:26):My policy is to avoid backporting PRs with overlay as much as possible.
Last updated: Jun 11 2023 at 01:30 UTC