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 /plugins/xml/doubleTypeInference.ml | |
| 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
Diffstat (limited to 'plugins/xml/doubleTypeInference.ml')
0 files changed, 0 insertions, 0 deletions