Skip to content

Fix dune-project

Lennard Gäherrequested to merge
lennard/fix-dune-project into main

The generated comment in the dune-project file wasn't good. Also generate it in the workdir instead of the output dir instead.

Merge request reports