From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 11 Feb 2004 11:11:49 +0000 (+0000)
Subject: - make *opt fixed
X-Git-Tag: V_0_3_0~30
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8efc118083312d8cef7ea080e7b4f780cae5979a;p=helm.git

- make *opt fixed
- added -vars -varsprefix cic:/Coq to testlibrary
---

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index b4446b8f3..56593b9c7 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -18,7 +18,7 @@ OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
 OCAMLFIND = ocamlfind
 OCAMLDEBUGOPTIONS = -g
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS)
-OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS)
+OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
 OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o
 OCAMLDEBUG = wowcamldebug
 
@@ -85,14 +85,14 @@ testlibrary: $(TESTLIBOBJS) $(TEST_LIBRARIES)
 	$(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) -linkpkg \
 		-package "$(TEST_REQUIRES)" -o $@ $(TESTLIBOBJS)
 testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT)
-	$(OCAMLFIND) opt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
+	$(OCAMLFIND) ocamlopt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
 		$(TESTLIBOBJS:.cmo=.cmx)
 
 regtest: $(REGTESTOBJS) $(TEST_LIBRARIES)
 	$(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) -linkpkg \
 		-package "$(TEST_REQUIRES)" -o $@ $(REGTESTOBJS)
 regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT)
-	$(OCAMLOPT) opt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
+	$(OCAMLFIND) ocamlopt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
 		$(REGTESTOBJS:.cmo=.cmx)
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx
@@ -127,7 +127,7 @@ test: regtest
 envtest: regtest
 	./regtest -dump $(INTESTS) 2> /dev/null
 librarytest: testlibrary.opt
-	./testlibrary.opt index.txt 2>/dev/null >LOG &
+	./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG &
 
 MAIN = ./gTopLevel
 ARGS =