From 7dd58fcb365a74778e22e673d01acdf09953f95e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 13 Feb 2025 15:43:59 +0100
Subject: [PATCH] test suite fix approve-output target

---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 16ea90e3aa..ea1a0318e7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -300,7 +300,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	$(HIDE)$(call REPORT_TIMER,$@)
 
 .PHONY: approve-output
-approve-output: output output-coqtop output-coqchk
+approve-output: output
 	$(HIDE)for f in $(addsuffix /*.out.real,$^); do if [ -f "$$f" ]; then \
 	  mv "$$f" "$${f%.real}"; \
 	  echo "Updated $${f%.real}!"; \