diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-15 15:42:14 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-15 15:42:14 +0100 |
| commit | 83023733e8ac5fa28893b260664f6d6527b481ab (patch) | |
| tree | f95debbe0c1daf2ef6e8f6cbe2443215cd4ecf37 /Makefile.extr | |
| parent | 5aecefe808aaaad6ab05037e7d5e7f53b53e0b94 (diff) | |
| download | compcert-83023733e8ac5fa28893b260664f6d6527b481ab.tar.gz compcert-83023733e8ac5fa28893b260664f6d6527b481ab.zip | |
Added variable to the Makefile to specify additional linker commands and changed the configure script to deactivated the checklink build if needed.
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 35ae5f7b..70b0cb67 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) $+ + @$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC) ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC) ifeq ($(CCHECKLINK),true) |