aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-01-15 15:42:14 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-01-15 15:42:14 +0100
commit83023733e8ac5fa28893b260664f6d6527b481ab (patch)
treef95debbe0c1daf2ef6e8f6cbe2443215cd4ecf37 /Makefile
parent5aecefe808aaaad6ab05037e7d5e7f53b53e0b94 (diff)
downloadcompcert-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')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 6ed50ce2..b4db7be9 100644
--- a/Makefile
+++ b/Makefile
@@ -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
+ ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml $(LINKERSPEC)
tools/modorder: tools/modorder.ml
- ocamlopt -o tools/modorder str.cmxa tools/modorder.ml
+ ocamlopt -o tools/modorder str.cmxa tools/modorder.ml $(LINKERSPEC)
latexdoc:
cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)