Niels van der Weide
Niels van der Weide
> What would be the fix for such warnings? Removing one of the two notations? I think that the error comes from the fact that the notations have different priorities....
This seems to work. So, the changes are as follows: - When a PR is a draft, the CI does not run - When a PR is marked 'ready for...
> How can CI be triggered? Maybe only by a dummy commit? The CI has been triggered.
> Do I see it right that a number of checks is not being run now? I see nothing for Apple computers and no Coq 8.19/8.20. Yes. We removed those...
> I parially agree. One downside is that Alectryon only runs on coq 8.20 (I believe), because it cannot handle the switch to a different interface with rocq 9. Another...
> That would work. How do you feel about the fact that the rocq devs already do not compile it anymore, and now it will also be omitted by alectryon?...