Stream: Coq devs & plugin devs

Topic: ci-template vs ci-template-flambda

Jason Gross (Sep 10 2023 at 18:24):

When adding new CI jobs, what's the preferred default template to extend? ci-template? ci-template-flambda?

Gaëtan Gilbert (Sep 10 2023 at 20:05):

no preference

Emilio Jesús Gallego Arias (Sep 11 2023 at 20:12):

Are the differences documented?

Last updated: Nov 29 2023 at 21:01 UTC