diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-20 16:50:07 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-20 16:50:07 +0100 |
| commit | b0c09b32f3e559ca22afc4dc40fdd60964cb3292 (patch) | |
| tree | 84d35a635567f7d348abd29f5688e29daee2f449 | |
| parent | 860e340b9a383964773d9c4523fb02a1de407e7f (diff) | |
| download | compcert-kvx-b0c09b32f3e559ca22afc4dc40fdd60964cb3292.tar.gz compcert-kvx-b0c09b32f3e559ca22afc4dc40fdd60964cb3292.zip | |
Removed the linker flag again.
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | Makefile.extr | 4 |
2 files changed, 4 insertions, 4 deletions
@@ -174,9 +174,9 @@ doc/coq2html.ml: doc/coq2html.mll ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml $(LINKERSPEC) + ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml tools/modorder: tools/modorder.ml - ocamlopt -o tools/modorder str.cmxa tools/modorder.ml $(LINKERSPEC) + ocamlopt -o tools/modorder str.cmxa tools/modorder.ml latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) 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) |