Commit 74fae80b authored by MARCHE Claude's avatar MARCHE Claude

make bench should removed generated why3shapes.gz

parent 2325f49a
......@@ -1560,17 +1560,17 @@ test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa
test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma lib/why3/why3session.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma lib/why3/why3session.cma $< > /dev/null\
|| (rm -f why3session.xml why3shapes.dat why3shapes.gz; \
|| (rm -f why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f why3session.xml
@rm -f why3session.xml why3shapes why3shapes.gz
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa lib/why3/why3session.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa lib/why3/why3session.cmxa $< \
&& ./test-session.opt > /dev/null) \
|| (rm -f test-session.opt why3session.xml why3shapes.dat why3shapes.gz; \
|| (rm -f test-session.opt why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f test-session.opt why3session.xml
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte -I lib/coq-tactic/ bench/coq-tactic/test.v
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment