diff options
| author | Gaëtan Gilbert | 2019-02-05 15:34:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-06 11:17:49 +0100 |
| commit | f29aa6720eba884533972530b4283bf19d8410aa (patch) | |
| tree | 8f48cdb1cf3ccf5218cc7597000675514085ae06 /Makefile.vofiles | |
| parent | 37b900aeda68ae1e067a7770c16c11ea327a14dc (diff) | |
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
Diffstat (limited to 'Makefile.vofiles')
| -rw-r--r-- | Makefile.vofiles | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Makefile.vofiles b/Makefile.vofiles index d5217ef4b7..a71d68e565 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -42,7 +42,10 @@ GLOBFILES:=$(ALLVO:.$(VO)=.glob) endif ifdef NATIVECOMPUTE -NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO)) +NATIVEFILES := $(call vo_to_cm,$(ALLVO)) +ifeq ($(BEST),opt) +NATIVEFILES += $(call vo_to_obj,$(ALLVO)) +endif else NATIVEFILES := endif @@ -50,5 +53,5 @@ LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES) # For emacs: # Local Variables: -# mode: makefile +# mode: makefile-gmake # End: |