aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorsacerdot2000-11-27 15:59:18 +0000
committersacerdot2000-11-27 15:59:18 +0000
commit4e990ab6bf33b5667930f7bcae970d5c3b29ef94 (patch)
tree97cc7e953a933b0b35fcd39a2b79ff8a752161af /Makefile
parent7b6eff67e52128871d637630ab37a9f051b95fdd (diff)
Xml contrib retached
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@995 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 3 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index eb846cffdb..c60a08eb33 100644
--- a/Makefile
+++ b/Makefile
@@ -127,8 +127,8 @@ USERTACCMX=$(USERTAC:.ml4=.cmx)
CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
contrib/ring/quote.cmo contrib/ring/ring.cmo \
-# contrib/xml/xml.cmo \
-# contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
+ contrib/xml/xml.cmo \
+ contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
CMA=$(CLIBS) $(CAMLP4OBJS)
CMXA=$(CMA:.cma=.cmxa)
@@ -338,8 +338,7 @@ RINGVO = contrib/ring/ArithRing.vo contrib/ring/Ring_normalize.vo \
contrib/ring/ZArithRing.vo contrib/ring/Ring_abstract.vo \
contrib/ring/Quote.vo
-#XMLVO = contrib/xml/Xml.vo
-XMLVO=
+XMLVO = contrib/xml/Xml.vo
CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO)