Stream: Dune devs & users

Topic: not failing builds on warnings


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 04:02 UTC