aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.build9
1 files changed, 6 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build
index c8b4fa5f17..41c5c051af 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -624,7 +624,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
@@ -633,7 +633,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
@@ -644,11 +644,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