From bc4fce093271cda274d7edb3a8dc1d709c9a5968 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Sep 2024 19:46:50 +0200
Subject: [PATCH] sync dune flags
---
dune | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/dune b/dune
index 822f87d0..98673015 100644
--- a/dune
+++ b/dune
@@ -4,4 +4,5 @@
(flags ; Configure the coqc flags.
(:standard ; Keeping the default flags.
; Add custom flags (to be kept in sync with _CoqProject).
- -w -argument-scope-delimiter)))))
+ -w -argument-scope-delimiter
+ -w -notation-incompatible-prefix)))))
--
GitLab