aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Boutillier2014-03-06 18:20:07 +0100
committerPierre Boutillier2014-03-06 18:20:07 +0100
commit7639e423db4174787b1eeb2647f31539cfaa3326 (patch)
tree6d871b73fd3d85cdbdd368c709d44124efc03c16
parentc3e6866b05a0360946e93fed5ea8828b76586d4e (diff)
make install-coqlight installs DLLCOQRUN and LIBCOQRUN
-rw-r--r--Makefile.build4
1 files changed, 4 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build
index 7bfc6f9539..363f5574e7 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -673,7 +673,11 @@ install-library-light:
$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
rm -f $(FULLCOQLIB)/revision
-$(INSTALLLIB) revision $(FULLCOQLIB)
+ifndef CUSTOM
+ $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
+endif
ifeq ($(BEST),opt)
+ $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
$(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT)
endif