diff options
| author | notin | 2007-10-18 21:45:40 +0000 |
|---|---|---|
| committer | notin | 2007-10-18 21:45:40 +0000 |
| commit | a931f2340192b62de9cae3f5850bfc33bde9b88f (patch) | |
| tree | c2ba5681aff331b79b80b1f3e24c44b211266658 | |
| parent | fec743673b79a42f679d087fb0b8e845d06ff3aa (diff) | |
Intallation des .cma/.cmxa
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10241 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 10 | ||||
| -rw-r--r-- | Makefile.common | 3 |
2 files changed, 4 insertions, 9 deletions
diff --git a/Makefile.build b/Makefile.build index 3cea8b8a41..0a2186899f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -602,14 +602,6 @@ 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 \ @@ -619,7 +611,7 @@ install-library: $(MKDIR) $(FULLCOQLIB)/states cp states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib - cp $(OBJECTCMA) $(OBJECTCMXA) $(GRAMMARCMA) $(FULLCOQLIB) + cp $(LINKCMO) $(LINKCMOCMXA) $(GRAMMARCMA) $(FULLCOQLIB) install-library-light: $(MKDIR) $(FULLCOQLIB) diff --git a/Makefile.common b/Makefile.common index 3cff1c7620..004cef6406 100644 --- a/Makefile.common +++ b/Makefile.common @@ -270,6 +270,7 @@ CMXA:=$(CMA:.cma=.cmxa) # Beware that highparsing.cma should appear before hightactics.cma # respecting this order is useful for developers that want to load or link # the libraries directly + LINKCMO:=$(CONFIG) 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 \ @@ -382,6 +383,8 @@ GRAMMARSCMO:=\ GRAMMARCMO:=$(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO) +GRAMMARCMA:=parsing/grammar.cma + GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \ parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \ parsing/g_prim.ml4 parsing/g_tactic.ml4 \ |