Skip to content

Remove build directories by default

Remove build directories by default. This is already the tested case on the nightly builds, see infrastructure/dune-nightly-test!8 (closed).. So, this setting would also test this for local CIs.

Merge request reports

Loading