Karl Palmskog (May 28 2020 at 16:56): Karl Palmskog (May 28 2020 at 16:56):possibly the least intuitive build command I've ever used: dune build --profile release. Is there a reason there isn't some more intuitive alias for ignoring warnings?
Emilio Jesús Gallego Arias (May 28 2020 at 17:03):If you want to tweak the default set of fatal warnings for the dev profile indeed you can modify it using the (env ...) stanza https://dune.readthedocs.io/en/stable/dune-files.html#env
Emilio Jesús Gallego Arias (May 28 2020 at 17:04):Default warning flags in the dev profile are indeed pretty strict, that was discussed upstream, but it was decided to keep the default like this
Emilio Jesús Gallego Arias (May 28 2020 at 17:05):A part of the dune philosophy is that builds should be totally free of noise, so indeed that's one the reasons for the strict default
Last updated: Jun 04 2023 at 22:30 UTC