Michael Soegtrop (Jan 23 2022 at 15:10): Michael Soegtrop (Jan 23 2022 at 15:10):@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.
Karl Palmskog (Jan 23 2022 at 15:14):@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