aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-02-02 11:25:04 +0000
committerGravatar bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-02-02 11:25:04 +0000
commita5891b65557e35477a8a560b433deaca0f5ffdd5 (patch)
tree430c6b76a7ee30f2c48bacd0ecc9d718059a48e7 /Makefile
parent69bd1551398721d78a35f7f537df70c0b799ca1e (diff)
reorganize the order of librairies in the entry CMO to make sure this can
be used as a reference to know in which order the libraries should be loaded git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5278 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 5 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 9ecc26407..60b4e296b 100644
--- a/Makefile
+++ b/Makefile
@@ -296,11 +296,14 @@ CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
CMA=$(CLIBS) $(CAMLP4OBJS)
CMXA=$(CMA:.cma=.cmxa)
+# Beware that highparsingnew.cma should appear before hightactics.cma
+# respecting this order is useful for developers that want to load or link
+# the libraries directly
CMO=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \
pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma \
proofs/proofs.cma tactics/tactics.cma toplevel/toplevel.cma \
- parsing/highparsing.cma tactics/hightactics.cma \
- contrib/contrib.cma parsing/highparsingnew.cma
+ parsing/highparsing.cma parsing/highparsingnew.cma tactics/hightactics.cma \
+ contrib/contrib.cma
CMOCMXA=$(CMO:.cma=.cmxa)
CMX=$(CMOCMXA:.cmo=.cmx)