diff --git a/tools/bin/dune b/tools/bin/dune index e304573e3..674eca5b6 100644 --- a/tools/bin/dune +++ b/tools/bin/dune @@ -11,4 +11,4 @@ (name main) (libraries tools) (flags - (-w "+6+26+27+32+33+39"))) + (:standard -w "+6+26+27+32+33+39")))