Stream: Coq Platform devs & users

Topic: Opam dev packages

view this post on Zulip 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.

view this post on Zulip 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.,


Last updated: Apr 14 2024 at 10:39 UTC