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

1 files changed, 2 insertions, 1 deletions

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"