Skip to content

Remove generated files and associated CI checks.

Rodolphe Lepigre requested to merge ci/no_generated_files into master

This requires adding an option [--soft] to [refinedc clean] in order to prevent the [_CoqProject] file to be edited locally when building or cleaning the examples.

No sure we want to merge that, what do you think @msammler?

Merge request reports

Loading