diff options
| -rw-r--r-- | Makefile.build | 28 | ||||
| -rw-r--r-- | Makefile.common | 5 |
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 |