diff options
Diffstat (limited to 'otherlibs/dynlink/Makefile')
| -rw-r--r-- | otherlibs/dynlink/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/dynlink/Makefile b/otherlibs/dynlink/Makefile index 41e33d5449..644ab12199 100644 --- a/otherlibs/dynlink/Makefile +++ b/otherlibs/dynlink/Makefile @@ -30,7 +30,7 @@ OCAMLOPT=$(BEST_OCAMLOPT) -g -nostdlib -I $(ROOTDIR)/stdlib # COMPFLAGS should be in sync with the toplevel Makefile's COMPFLAGS. COMPFLAGS=-strict-sequence -principal -absname \ -w +a-4-9-40-41-42-44-45-48-66-70 \ - -warn-error +A \ + -warn-error +A \ -bin-annot -safe-string -strict-formats ifeq "$(FLAMBDA)" "true" OPTCOMPFLAGS += -O3 |