From bcc012e553ded1855653dc6fbc15875749213f83 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 19 Aug 2020 15:14:07 -0400 Subject: Improve `make approve-output` It now silently does nothing rather than erroring with `mv: cannot stat 'output/*.out.real': No such file or directory` if there is no output to approve, and also correctly handles `output-coqtop` and `output-coqchk` rather than ignoring these directories. Fixes #12863 --- .../11-infrastructure-and-dependencies/12864-fix-approve-output.rst | 5 +++++ test-suite/Makefile | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) create mode 100644 doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst diff --git a/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst new file mode 100644 index 0000000000..c754826e62 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst @@ -0,0 +1,5 @@ +- **Fixed:** + ``make approve-output`` in the test-suite now correctly handles + ``output-coqtop`` and ``output-coqchk`` tests (`#12864 + `_, fixes `#12863 + `_, by Jason Gross). diff --git a/test-suite/Makefile b/test-suite/Makefile index f7447d6cec..6f49ae0d83 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -501,8 +501,8 @@ $(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISI } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi .PHONY: approve-output -approve-output: output output-coqtop - $(HIDE)for f in output/*.out.real; do \ +approve-output: output output-coqtop output-coqchk + $(HIDE)for f in $(wildcard $(addsuffix /*.out.real,$^)); do \ mv "$$f" "$${f%.real}"; \ echo "Updated $${f%.real}!"; \ done -- cgit v1.2.3