From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 27 Nov 2008 10:34:26 +0000 (+0000)
Subject: new kernel is compiled since the META of grafite_parser depends on the META of ng_dis... 
X-Git-Tag: make_still_working~4494
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8b95f91af568cfe587b3f05b9c111c6ebe8b0a8;p=helm.git

new kernel is compiled since the META of grafite_parser depends on the META of ng_disambiguation
---

diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile
index 01dabc9a6..afe6c3f82 100644
--- a/helm/software/components/Makefile
+++ b/helm/software/components/Makefile
@@ -33,6 +33,9 @@ MODULES =			\
 	cic_disambiguation	\
 	lexicon			\
 	grafite_engine          \
+	ng_kernel		\
+	ng_refiner		\
+	ng_disambiguation	\
 	grafite_parser          \
 	tptp_grafite            \
 	$(NULL)
diff --git a/helm/software/components/ng_disambiguation/Makefile b/helm/software/components/ng_disambiguation/Makefile
index 3bac09451..411b10feb 100644
--- a/helm/software/components/ng_disambiguation/Makefile
+++ b/helm/software/components/ng_disambiguation/Makefile
@@ -12,7 +12,7 @@ EXTRA_OBJECTS_TO_CLEAN =
 %.cmi: OCAMLOPTIONS += -w Ae
 %.cmx: OCAMLOPTIONS += -w Ae
 
-all: rt check
+all: 
 %: %.ml $(PACKAGE).cma
 	$(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $<
 all.opt opt: rt.opt check.opt