From 09279a529dc1fd3f0abd87e5430f597a0a8ef3d4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Sep 2024 19:47:24 +0200
Subject: [PATCH] sync dune flags
---
dune | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/dune b/dune
index d41346d5e..eab1d7fd8 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
+)))))
--
GitLab