aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
authorbarras2008-12-11 15:51:20 +0000
committerbarras2008-12-11 15:51:20 +0000
commit5a365ec9d7426663324a96a4f41882e787b048fa (patch)
treea2956f63505520ea8a2bc838735a30f375bdd111 /Makefile.build
parent59e84427c1ab59c8c03634d565a5f6117ab3f19f (diff)
do not install coqchk cmi files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11666 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index 41e91f0af5..bba84709bd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -504,7 +504,7 @@ install-pcoq-manpages:
validate:: $(BESTCHICKEN) $(ALLVO)
$(SHOW)'COQCHK <theories & contrib>'
- $(BESTCHICKEN) -boot -o -m $(ALLMODS)
+ $(HIDE)$(BESTCHICKEN) -boot -o -m $(ALLMODS)
check:: world
cd test-suite; \
@@ -669,7 +669,7 @@ install-library:
ifeq ($(BEST),opt)
$(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB)
endif
- find . $(FIND_VCS_CLAUSE) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
+ find . $(FIND_VCS_CLAUSE) $(PRUNE_CHECKER) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
# csdpcert is not meant to be directly called by the user; we install
# it with libraries
-$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega