From 207f75840f870a28f1959e1c256405d80829c007 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 4 Oct 2012 22:08:13 +0000
Subject: Repaired configure damaged in r15748 for those bash users which have
 CDPATH variable set. Indeed, command cd is verbose when CDPATH is set, what
 would introduce garbage in the generated file config/coq_config.ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15855 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 configure | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'configure')

diff --git a/configure b/configure
index 874818aaec..25acccb8a3 100755
--- a/configure
+++ b/configure
@@ -1031,8 +1031,9 @@ let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
 END_OF_COQ_CONFIG
 
 # Subdirectories of theories/ added in coq_config.ml
+# Note: don't propagate output of cd if any: it's verbose when CDPATH is defined
 subdirs () {
-    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) ) >> "$mlconfig_file"
+    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) >> "$mlconfig_file")
 }
 
 echo "let theories_dirs = [" >> "$mlconfig_file"
-- 
cgit v1.2.3