Skip to content

Remove build directories by default

Santiago Ospina De Los Ríos requested to merge feature/remove-build-directories into master

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