changed deps since testlibrary now uses (minimally) BatchParser

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 4017367da8f2e04152429789064fb2a79474fffe..8b89d823a18cd92a894456d40d1d7977ea9e8ffd 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -38,22 +38,30 @@ stop:
        $(MAKE) -C ../hbugs/ stop
 
 INTERFACE_FILES = \
-       proofEngine.mli logicalOperations.mli oldDisambiguate.mli \
-  disambiguatingParser.mli termEditor.mli texTermEditor.mli xmlDiff.mli \
-  chosenTransformer.mli termViewer.mli invokeTactics.mli hbugs.mli \
-  chosenTermEditor.mli 
+       proofEngine.mli \
+       logicalOperations.mli \
+       oldDisambiguate.mli \
+       disambiguatingParser.mli \
+       termEditor.mli \
+       texTermEditor.mli \
+       xmlDiff.mli \
+       chosenTransformer.mli \
+       termViewer.mli \
+       invokeTactics.mli \
+       hbugs.mli \
+       chosenTermEditor.mli 
 
 DEPOBJS = \
        $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
        gTopLevel.ml regtest.ml testlibrary.ml batchParser.ml batchParser.mli
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo
-REGTESTOBJS = \
+TESTOBJS = \
        oldDisambiguate.cmo \
        disambiguatingParser.cmo \
-       batchParser.cmo \
-       regtest.cmo
-TESTLIBOBJS = testlibrary.cmo
+       batchParser.cmo
+REGTESTOBJS = $(TESTOBJS) regtest.cmo
+TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo
 
 $(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES)
 $(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT)
@@ -121,7 +129,7 @@ test: regtest
 envtest: regtest
        ./regtest -dump $(INTESTS) 2> /dev/null
 librarytest: testlibrary.opt
-       ./testlibrary.opt - <index.txt 2>/dev/null >LOG &
+       ./testlibrary.opt index.txt 2>/dev/null >LOG &
 
 MAIN = ./gTopLevel
 ARGS =