aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-03 09:43:07 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-03 09:43:07 +0000
commitaf188f7c62ae3cca7620f3738a264c70d2c56597 (patch)
treea80cbd235bb154eece7f1d0351f497215eef3d31
parentf4222f57a430d71c26ecc3908ca069866a8f5ce1 (diff)
Fix the installation of plugins (both initial and late ones)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11876 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build28
-rw-r--r--Makefile.common5
2 files changed, 13 insertions, 20 deletions
diff --git a/Makefile.build b/Makefile.build
index c92cd29ad..d7957bde8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -636,15 +636,8 @@ FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
install-coq: install-binaries install-library install-coq-info
install-coqlight: install-binaries install-library-light
-install-binaries:: install-$(BEST) install-tools install-plugins-$(BEST)
+install-binaries:: install-$(BEST) install-tools
-install-plugins-byte::
- $(MKDIR) $(FULLCOQLIB)
- if $(HASNATDYNLINK) = true ; then cp --parents $(INITPLUGINS) $(FULLCOQLIB); fi
-
-install-plugins-opt::
- $(MKDIR) $(FULLCOQLIB)
- if $(HASNATDYNLINK) = false; then cp --parents $(INITPLUGINSOPT) $(FULLCOQLIB); fi
install-byte::
$(MKDIR) $(FULLBINDIR)
$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
@@ -665,10 +658,9 @@ install-tools::
install-library:
$(MKDIR) $(FULLCOQLIB)
- for f in $(LIBFILES); do \
- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
- $(INSTALLLIB) $$f $(FULLCOQLIB)/`dirname $$f`; \
- done
+ $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES)
+ $(INSTALLSH) $(FULLCOQLIB) $(PLUGINS)
+ $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
$(MKDIR) $(FULLCOQLIB)/states
$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLCOQLIB)/user-contrib
@@ -686,18 +678,14 @@ endif
install-library-light:
$(MKDIR) $(FULLCOQLIB)
- for f in $(LIBFILESLIGHT); do \
- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
- $(INSTALLLIB) $$f $(FULLCOQLIB)/`dirname $$f`; \
- done
+ $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT)
+ $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINS)
+ $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT)
$(MKDIR) $(FULLCOQLIB)/states
$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
install-allreals::
- for f in $(ALLREALS); do \
- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
- $(INSTALLLIB) $$f $(FULLCOQLIB)/`dirname $$f`; \
- done
+ $(INSTALLSH) $(FULLCOQLIB) $(ALLREALS)
install-coq-info: install-coq-manpages install-emacs install-latex
diff --git a/Makefile.common b/Makefile.common
index 8f6e1b808..a74126dfe 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -347,7 +347,12 @@ ifneq ($(HASNATDYNLINK),false)
CONTRIBSTATIC:=$(SUBTACCMO)
INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
$(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA)
+ PLUGINS:=$(INITPLUGINS) \
+ $(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
+ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \
+ $(FOURIERCMA) $(RTAUTOCMA)
INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ PLUGINSOPT:=$(PLUGINS:.cma=.cmxs)
ifeq ($(BEST),opt)
INITPLUGINSBEST:=$(INITPLUGINSOPT)
else