Skip to content
GitLab

Build: remove -O3 from dune file

Merged E. Rivas requested to merge er433/fix/O3 into dev

dune runs with release profile when using -p, but -O3 fails, thus removing it from dune file.

  • has a changelog entry
Edited by E. Rivas