summaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
commit61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch)
treed88d05baf35b9b09a034233300f35a694f9fa6c2 /Makefile.build
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build14
1 files changed, 8 insertions, 6 deletions
diff --git a/Makefile.build b/Makefile.build
index 59ee457c..41dfabbf 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -318,7 +318,7 @@ $(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT)
$(STRIP) $@
$(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE)
- $(SHOW)'OCAMLOPT -o $@'
+ $(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\
str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)
@@ -446,7 +446,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
# 3) plugins
###########################################################################
-.PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction
+.PHONY: plugins omega micromega ring setoid_ring nsatz xml extraction
.PHONY: field fourier funind cc subtac rtauto pluginsopt
plugins: $(PLUGINSVO)
@@ -455,7 +455,6 @@ micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
ring: $(RINGVO) $(RINGCMA)
setoid_ring: $(NEWRINGVO) $(NEWRINGCMA)
nsatz: $(NSATZVO) $(NSATZCMA)
-dp: $(DPCMA)
xml: $(XMLVO) $(XMLCMA)
extraction: $(EXTRACTIONCMA)
field: $(FIELDVO) $(FIELDCMA)
@@ -623,7 +622,7 @@ INSTALLCMI = $(sort \
install-library:
$(MKDIR) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT)
+ $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
$(MKDIR) $(FULLCOQLIB)/states
$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLCOQLIB)/user-contrib
@@ -632,7 +631,7 @@ install-library:
$(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI)
ifeq ($(BEST),opt)
$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a)
+ $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT)
endif
# csdpcert is not meant to be directly called by the user; we install
# it with libraries
@@ -643,11 +642,14 @@ endif
install-library-light:
$(MKDIR) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(INITPLUGINSOPT)
+ $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
$(MKDIR) $(FULLCOQLIB)/states
$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
rm -f $(FULLCOQLIB)/revision
-$(INSTALLLIB) revision $(FULLCOQLIB)
+ifeq ($(BEST),opt)
+ $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT)
+endif
install-coq-info: install-coq-manpages install-emacs install-latex