aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2023-03-06 16:05:43 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2023-03-06 16:05:57 +0100
commit1a7b93078eb531a6e9e5d4dc02bec143605c2264 (patch)
treed9c73f6e33b22fa8e151b9b81f17392fb6d16017
parenta6e44cd88d2b37a7747d5057d04834c0deaa6601 (diff)
downloadcompcert-1a7b93078eb531a6e9e5d4dc02bec143605c2264.tar.gz
compcert-1a7b93078eb531a6e9e5d4dc02bec143605c2264.zip
Include `+unix` and `+str` for OCaml 5 compatibility
In OCaml 5, the Unix and Str libraries are installed in subdirectories of the standard library directory. In OCaml 4, the `-I +str` and `-I +unix` options have no effect.
-rw-r--r--Makefile.extr4
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile.extr b/Makefile.extr
index 6035eb9a..7d020c8b 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -64,7 +64,9 @@ else
WARN_ERRORS=
endif
-COMPFLAGS+=-g -strict-sequence -safe-string $(INCLUDES) -I "$(MENHIR_DIR)" $(WARNINGS) $(WARN_ERRORS)
+COMPFLAGS+=-g -strict-sequence -safe-string \
+ $(INCLUDES) -I "$(MENHIR_DIR)" -I +str -I +unix \
+ $(WARNINGS) $(WARN_ERRORS)
# Using .opt compilers if available