diff --git a/dune b/dune index d41346d5e56b4a272afab0f543ac6d0ec7afdb57..eab1d7fd8ebcad40631757a45919b3e9b08a57ba 100644 --- a/dune +++ b/dune @@ -7,4 +7,6 @@ -w -notation-overridden -w -redundant-canonical-projection -w -unknown-warning - -w -argument-scope-delimiter))))) + -w -argument-scope-delimiter + -w -notation-incompatible-prefix +)))))