From f29aa6720eba884533972530b4283bf19d8410aa Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Feb 2019 15:34:49 +0100
Subject: Makefiles: Fixes for byte compilation

- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files

cf https://github.com/coq/coq/issues/9464
---
 Makefile.common | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 8292158ef8..bd0e19cd00 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -75,10 +75,12 @@ endif
 # for Declare ML Module files.
 
 ifeq ($(BEST),opt)
+TOPBIN:=$(TOPBINOPT)
 COQTOPBEST:=$(COQTOPEXE)
 DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 else
+TOPBIN:=$(TOPBYTE)
 COQTOPBEST:=$(COQTOPBYTE)
 DYNOBJ:=.cmo
 DYNLIB:=.cma
-- 
cgit v1.2.3