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?
For deprecation warnings, we could imagine some downstream developments treating them as errors (although unlikely).
didn't aac tactics treat deprecation as error? or was that only the plugin part?
@Gaëtan Gilbert the Coq part of AAC tactics (which uses the plugin) will indeed treat deprecation as error.
if this is a problem I can change it, but otherwise I'd like to keep it as a canary for deprecations
Only documentation PRs: fine to merge with just light CI.
Last updated: Sep 25 2023 at 14:01 UTC