]> matita.cs.unibo.it Git - helm.git/commitdiff
- make *opt fixed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 11 Feb 2004 11:11:49 +0000 (11:11 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 11 Feb 2004 11:11:49 +0000 (11:11 +0000)
- added -vars -varsprefix cic:/Coq to testlibrary

helm/gTopLevel/Makefile

index b4446b8f35d5ae64e36625a88828c5f5064a4acc..56593b9c76ddac5e9edaf8e932221624c3636a5c 100644 (file)
@@ -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 =