no longer build oldDisambiguate

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index 82b678e1e78f80a3ed0490eb9f21ca6fcd34a10f..d1cda56b31a1d331e8f58e87b65d4a722e34bed2 100644 (file)
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -7,10 +7,8 @@ proofEngine.cmo: proofEngine.cmi
 proofEngine.cmx: proofEngine.cmi 
 logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi 
 logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi 
-oldDisambiguate.cmo: oldDisambiguate.cmi 
-oldDisambiguate.cmx: oldDisambiguate.cmi 
-disambiguatingParser.cmo: oldDisambiguate.cmi disambiguatingParser.cmi 
-disambiguatingParser.cmx: oldDisambiguate.cmx disambiguatingParser.cmi 
+disambiguatingParser.cmo: disambiguatingParser.cmi 
+disambiguatingParser.cmx: disambiguatingParser.cmi 
 termEditor.cmo: disambiguatingParser.cmi termEditor.cmi 
 termEditor.cmx: disambiguatingParser.cmx termEditor.cmi 
 texTermEditor.cmo: disambiguatingParser.cmi texTermEditor.cmi 

diff --git a/helm/gTopLevel/Makefile.in b/helm/gTopLevel/Makefile.in
index 82c3d28212cd8a702e1b9abaf3e70f4f522cef6e..42dd44be1f8f29971aceddcb33846da36806a712 100644 (file)
--- a/helm/gTopLevel/Makefile.in
+++ b/helm/gTopLevel/Makefile.in
@@ -7,12 +7,11 @@ TEST_REQUIRES = \
        helm-tactics \
        helm-cic_transformations \
        helm-cic_textual_parser2 \
-       helm-cic_textual_parser \
-       helm-tex_cic_textual_parser \
        helm-xmldiff \
        lablgtk2 \
        mathml-editor \
-       lablgtkmathview
+       lablgtkmathview \
+       dbi.mysql
 
 REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
 
@@ -41,7 +40,6 @@ stop:
 INTERFACE_FILES = \
        proofEngine.mli \
        logicalOperations.mli \
-       oldDisambiguate.mli \
        disambiguatingParser.mli \
        termEditor.mli \
        texTermEditor.mli \
@@ -58,7 +56,6 @@ DEPOBJS = \
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo
 TESTOBJS = \
-       oldDisambiguate.cmo \
        disambiguatingParser.cmo \
        batchParser.cmo
 REGTESTOBJS = $(TESTOBJS) regtest.cmo