From a5ff2b91cd406e7acdeef18d1b1ee14a331ffdaa Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 13 Apr 2010 12:31:40 +0000
Subject: Remove only *.v.log files in clean of test-suite/Makefile

...so that "./check > check.log" works as expected.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12933 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 78cfad36f..e8b07c55a 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -92,7 +92,7 @@ clean:
 	rm -f trace lia.cache
 	$(SHOW) "RM        <**/*.stamp> <**/*.vo> <**/*.log>"
 	$(HIDE)find . \( \
-	  -name '*.stamp' -o -name '*.vo' -o -name '*.log' \
+	  -name '*.stamp' -o -name '*.vo' -o -name '*.v.log' \
 	\) -print0 | xargs -0 rm -f
 
 #######################################################################
-- 
cgit v1.2.3