diff options
Diffstat (limited to 'Makefile.extr')
| -rw-r--r-- | Makefile.extr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.extr b/Makefile.extr index 2afd6e31..5f02bf38 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -90,11 +90,11 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) ccomp: $(CCOMP_OBJS) @echo "Linking $@" - @$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC) + @$(OCAMLOPT) -o $@ $(LIBS) $+ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC) + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ ifeq ($(CCHECKLINK),true) |