aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-03-10 10:30:16 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-03-10 10:30:16 +0100
commite37e366c826a0dc422e449b9ad0afa70be204e12 (patch)
tree3bcc0c14099862614d19c95fee0edc7b388720b3 /Makefile
parent8aae10b50b321cfcbde86582cdd7ce1df8960628 (diff)
parent3e01154d693e1c457e1e974f5e9ebaa4601050aa (diff)
downloadcompcert-kvx-e37e366c826a0dc422e449b9ad0afa70be204e12.tar.gz
compcert-kvx-e37e366c826a0dc422e449b9ad0afa70be204e12.zip
Merge branch 'master' into dwarf
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile6
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 99fd7223..157fb1a2 100644
--- a/Makefile
+++ b/Makefile
@@ -174,15 +174,15 @@ 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)
%.vo: %.v
- @rm -f doc/glob/$(*F).glob
+ @rm -f doc/$(*F).glob
@echo "COQC $*.v"
@$(COQC) -dump-glob doc/$(*F).glob $*.v