From 6b854265e261b8c9e2e068364ef1405412b89063 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Wed, 15 Jul 2020 10:25:36 +0200
Subject: 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.
---
 Makefile | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 5e97ebbf..ae095a09 100644
--- a/Makefile
+++ b/Makefile
@@ -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)
-- 
cgit