aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-06 13:55:23 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-06 13:55:23 +0000
commitcf8ca10ab726face23cdd33a4c2bc9500cf0df40 (patch)
tree2ac7e817b7c9d616dde02597251be879d3419f58
parent64c9874e12872a08bfcce470b5e03813c5cff586 (diff)
Copie des .cmi en plus des .cma et des .cmxa
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11060 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build
index f2385dc44..97bab95df 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -658,6 +658,7 @@ install-library:
cp states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLCOQLIB)/user-contrib
cp $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB)
+ find . -name \*.cmi -exec cp {} $(FULLCOQLIB) \;
install-library-light:
$(MKDIR) $(FULLCOQLIB)