aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornotin2007-10-18 14:20:44 +0000
committernotin2007-10-18 14:20:44 +0000
commit762eebb37e05fbc8e91d6a8a88618c08aba52830 (patch)
tree42e5bafe8bd49d3492d98221a19b3bc76c652033
parent4781b722501dc1a730a11da477e36e4429bcd5f8 (diff)
Copie des .cma et des .cmxa, et de grammar.cma dans le répertoire de Coq (pour faciliter la compilation des tactiques ml par les utilisateurs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10238 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build9
1 files changed, 9 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build
index 35b7d429ec..3cea8b8a41 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -602,6 +602,14 @@ install-tools::
cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
cp $(TOOLS) $(FULLBINDIR)
+GRAMMARCMA=parsing/grammar.cma
+OBJECTCMA=lib/lib.cma kernel/kernel.cma library/library.cma \
+ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
+ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
+ parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma
+
+OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
+
install-library:
$(MKDIR) $(FULLCOQLIB)
for f in $(LIBFILES); do \
@@ -611,6 +619,7 @@ install-library:
$(MKDIR) $(FULLCOQLIB)/states
cp states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLCOQLIB)/user-contrib
+ cp $(OBJECTCMA) $(OBJECTCMXA) $(GRAMMARCMA) $(FULLCOQLIB)
install-library-light:
$(MKDIR) $(FULLCOQLIB)