diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-06 16:05:43 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-06 16:05:57 +0100 |
commit | 1a7b93078eb531a6e9e5d4dc02bec143605c2264 (patch) | |
tree | d9c73f6e33b22fa8e151b9b81f17392fb6d16017 | |
parent | a6e44cd88d2b37a7747d5057d04834c0deaa6601 (diff) | |
download | compcert-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.extr | 4 |
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 |