From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 12 Jan 2006 13:25:09 +0000 (+0000)
Subject: hgdome and xmldiff no longer compiled
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4829e693f115e4f6eacaa81d971e8730a4a4833a

hgdome and xmldiff no longer compiled
---

diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in
index 0c2d49411..fe18d792d 100644
--- a/helm/ocaml/Makefile.in
+++ b/helm/ocaml/Makefile.in
@@ -3,12 +3,10 @@ NULL =
 MODULES =			\
 	extlib			\
 	xml			\
-	hgdome			\
 	registry		\
  	hmysql 			\
 	utf8_macros		\
 	thread			\
-	xmldiff			\
 	urimanager		\
 	logger			\
 	getter			\