Skip to content

Commit 7dd58fc

Browse files
committed
test suite fix approve-output target
1 parent ddae606 commit 7dd58fc

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

test-suite/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -300,7 +300,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
300300
$(HIDE)$(call REPORT_TIMER,$@)
301301

302302
.PHONY: approve-output
303-
approve-output: output output-coqtop output-coqchk
303+
approve-output: output
304304
$(HIDE)for f in $(addsuffix /*.out.real,$^); do if [ -f "$$f" ]; then \
305305
mv "$$f" "$${f%.real}"; \
306306
echo "Updated $${f%.real}!"; \

0 commit comments

Comments
 (0)