From 7507d6e297a17a2dd1ff564343e5831e27222d7e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 20 Jun 2023 10:31:26 -0400 Subject: [PATCH] dune warning --- dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dune b/dune index 1c6b45f6..575b5a09 100644 --- a/dune +++ b/dune @@ -1,3 +1,3 @@ (env (_ - (flags :standard -warn-error -a+8 -w +a-4-30-40-41-42-44-70 -strict-sequence))) + (flags :standard -warn-error -a+8 -w +a-4-30-40-41-42-44-48-70 -strict-sequence)))