aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 2b668724..6ad272a8 100644
--- a/Makefile
+++ b/Makefile
@@ -41,6 +41,7 @@ OCB_OPTIONS=\
OCB_OPTIONS_CHECKLINK=\
$(OCB_OPTIONS) \
-I checklink \
+ -cflags "-w -3" \
-use-ocamlfind
OCB_OPTIONS_CLIGHTGEN=\
$(OCB_OPTIONS) \