aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common16
1 files changed, 8 insertions, 8 deletions
diff --git a/Makefile.common b/Makefile.common
index 920df2d2b5..acbc2feaab 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -855,9 +855,16 @@ DPVO:=$(addprefix contrib/dp/, \
RTAUTOVO:=$(addprefix contrib/rtauto/, \
Bintree.vo Rtauto.vo )
+ifneq ($(HASNATDYNLINK),false)
+INTERFACEVO:=contrib/interface/CoqInterface.vo
+else
+INTERFACEVO:=
+endif
+
CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
$(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
- $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO)
+ $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
+ $(INTERFACEVO)
ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
VFILES:= $(ALLVO:.vo=.v)
@@ -873,13 +880,6 @@ LIBFILESLIGHT:=$(THEORIESLIGHTVO)
## Specials
-ifneq ($(HASNATDYNLINK),false)
-INTERFACEVO:=contrib/interface/CoqInterface.vo
-else
-INTERFACEVO:=
-endif
-
-
MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
man/coqwc.1 man/coqdoc.1 man/coqide.1 \