diff options
| author | Jason Gross | 2020-08-19 15:14:07 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-08-19 15:16:13 -0400 |
| commit | bcc012e553ded1855653dc6fbc15875749213f83 (patch) | |
| tree | ae2d642a68c5712590b06958c1a1a18bab723328 /test-suite | |
| parent | b409b9837ce438042bb259d16a1b5156a2e0acb9 (diff) | |
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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
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 |