From bca1c03fb2fb6f531eee000f24d1bbfed0f5fb66 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 1 Jun 2018 11:50:38 +0200
Subject: test suite: make target to regenerate failing output tests

---
 test-suite/Makefile | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f41fb5b1e4..32e245e362 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
-- 
cgit v1.2.3