diff options
| -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 |