diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-01 11:50:38 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-04 16:00:07 +0200 |
commit | bca1c03fb2fb6f531eee000f24d1bbfed0f5fb66 (patch) | |
tree | b1bc29c5327c345eb1218905bb0ef92478cf8fe5 /test-suite/Makefile | |
parent | ac0bb15616550d00f5e6e7d6239e3b7ff2632975 (diff) |
test suite: make target to regenerate failing output tests
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r-- | test-suite/Makefile | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f41fb5b1e..32e245e36 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -362,26 +362,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ + output=$*.out.real; \ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^<W>" \ | sed 's/File "[^"]*"/File "stdin"/' \ - > $$tmpoutput; \ - diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \ + > $$output; \ + diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ + rm $$output; \ else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ $(FAIL); \ fi; \ - rm $$tmpoutput; \ } > "$@" +.PHONY: approve-output +approve-output: output + $(HIDE)for f in output/*.out.real; do \ + mv "$$f" "$${f%.real}"; \ + echo "Updated $${f%.real}!"; \ + done + # the expected output for the MExtraction test is # /plugins/micromega/micromega.ml except with additional newline output/MExtraction.out: ../plugins/micromega/micromega.ml |