diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-07-15 10:25:36 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-07-15 10:25:36 +0200 |
| commit | 6b854265e261b8c9e2e068364ef1405412b89063 (patch) | |
| tree | f123fe2203de10c7aa5fabf479c6c989f943f8e4 /Makefile | |
| parent | 13e0566dbdd8bf845d7c2a65ffefaaf460381e70 (diff) | |
| download | compcert-kvx-6b854265e261b8c9e2e068364ef1405412b89063.tar.gz compcert-kvx-6b854265e261b8c9e2e068364ef1405412b89063.zip | |
Bytecode-only build, continued
If ocamlopt is not available, use ocamlc instead of ocamlopt to build
auxiliary tools (tools/modorder, tools/ndfun).
This is a follow-up to commit 9af28924.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 9 |
1 files changed, 9 insertions, 0 deletions
@@ -191,9 +191,18 @@ documentation: $(FILES) $(filter-out doc/coq2html cparser/Parser.v, $^) tools/ndfun: tools/ndfun.ml +ifeq ($(OCAML_NATIVE_COMP),true) ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml +else + ocamlc -o tools/ndfun str.cma tools/ndfun.ml +endif + tools/modorder: tools/modorder.ml +ifeq ($(OCAML_NATIVE_COMP),true) ocamlopt -o tools/modorder str.cmxa tools/modorder.ml +else + ocamlc -o tools/modorder str.cma tools/modorder.ml +endif latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) |