diff options
| author | herbelin | 2012-10-04 22:08:13 +0000 |
|---|---|---|
| committer | herbelin | 2012-10-04 22:08:13 +0000 |
| commit | 207f75840f870a28f1959e1c256405d80829c007 (patch) | |
| tree | 528995aeb64d03858f9a9d1bc1521d4875dd6831 | |
| parent | d1fb79f4469eda2a15c79d14e1c292abb9d45adc (diff) | |
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
| -rwxr-xr-x | configure | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -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" |