diff options
| -rw-r--r-- | stdlib/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stdlib/Makefile b/stdlib/Makefile index 9a9d58823..d8020829e 100644 --- a/stdlib/Makefile +++ b/stdlib/Makefile @@ -109,7 +109,7 @@ oo.cmi: oo.mli # labelled modules require the -nolabels flag labelled.cmo: - $(MAKE) EXTRAFLAGS=-nolabels $(LABELLED:.ml=.cmo) + $(MAKE) EXTRAFLAGS=-nolabels COMPILER=$(COMPILER) $(LABELLED:.ml=.cmo) touch $@ labelled.cmx: $(MAKE) EXTRAFLAGS=-nolabels $(LABELLED:.ml=.cmx) |