Jason Gross (Nov 24 2022 at 03:47): Jason Gross (Nov 24 2022 at 03:47):Do PRs that only change deprecation warnings like https://github.com/coq/coq/pull/16892#issuecomment-1325919914, or PRs that only change documentation, need full CI?
Maxime Dénès (Nov 24 2022 at 08:29):For deprecation warnings, we could imagine some downstream developments treating them as errors (although unlikely).
Gaëtan Gilbert (Nov 24 2022 at 08:46):didn't aac tactics treat deprecation as error? or was that only the plugin part?
Karl Palmskog (Nov 24 2022 at 08:52):@Gaëtan Gilbert the Coq part of AAC tactics (which uses the plugin) will indeed treat deprecation as error.
Karl Palmskog (Nov 24 2022 at 08:53):if this is a problem I can change it, but otherwise I'd like to keep it as a canary for deprecations
Théo Zimmermann (Nov 24 2022 at 09:26):Only documentation PRs: fine to merge with just light CI.
Last updated: Sep 25 2023 at 14:01 UTC