Duplicate warning annotations

[JasonGross]

Since the CI update, we're getting duplicate warning annotations from the opam package jobs. I think this needs to be solved upstream at https://github.com/coq-community/docker-coq-action/issues/65 , and then we can update the configuration. cc docker coq action maintainers @erikmd,@Zimmi48, any hope of getting this solved soon?

[erikmd]

Hi @JasonGross, thanks for the ping! It happens we briefly discussed this with @Zimmi48 a few days ago :) we were not sure whether disabling warnings annotations would be a really useful feature (e.g. because very often it can be worth it to compare the warnings' text between various coq versions…) but anyway we agree to implement this! so I'm assigning the feature request https://github.com/coq-community/docker-coq-action/issues/65 ; I'm still busy this afternoon but I'll implement this as soon as I have released coqorg/coq:8.15-rc1.

[JasonGross]

Great, thanks! Btw, it might be useful to leave not just two values (on, off), but three, where the third one is multiline (perhaps even the default), based on https://github.com/coq-community/docker-coq-action/issues/55 (which has the downside that it may spin out of control and highlight way too much text if it misreads where the error terminator is).