@Karl Palmskog : I have a larger number of dev packages in my extra-dev patch repo (15 or so). Shall I push these to extra dev in a single PR with CI disabled or in separate PRs? They are reasonably well tested in Coq Platform CI and CIing dev packages anyway doesn't make that much sense.
@Michael Soegtrop sure, you can do a single PR, but maybe you can use the
ci-skip thing in your PR message, e.g.,
ci-skip: coq-flocq.dev coq-compcert.dev
Last updated: Jun 06 2023 at 22:01 UTC