aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-21 12:38:02 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-21 12:38:02 +0000
commitd5fc85b0b69b870b9dde5cc3b8faa5cbb5251881 (patch)
tree6998033532a9d520f62901fd4d37cda91d98290d /Makefile
parentfca3fc6fac26b88ce8abafad6f01a68e1b6f9d39 (diff)
XML débranché
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 25cbd8a7a..04ceabaf3 100644
--- a/Makefile
+++ b/Makefile
@@ -320,7 +320,8 @@ 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 = contrib/xml/Xml.vo
+XMLVO=
CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO)