diff options
| author | Gaëtan Gilbert | 2020-08-24 13:49:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-24 13:49:20 +0200 |
| commit | f42b28ed0cfd200395a4a32fd1ebe6a7f73a7ddb (patch) | |
| tree | 540e542c5e34d228e7ae4a55ac9c743a90d6328d /test-suite | |
| parent | 99e944f873589cf350e49f3bfda6094ffbfa545b (diff) | |
| parent | bcc012e553ded1855653dc6fbc15875749213f83 (diff) | |
Merge PR #12864: Improve `make approve-output`
Reviewed-by: SkySkimmer
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 7d219b6e8b..28add48b36 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -500,8 +500,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 |