diff options
| author | glondu | 2010-04-11 16:58:12 +0000 |
|---|---|---|
| committer | glondu | 2010-04-11 16:58:12 +0000 |
| commit | 328cd1cb92e463b2a9cdd669e7e31090dc905c64 (patch) | |
| tree | 96efe136562782c27692ed1aa1ff89899c8b9792 /dev/doc/debugging.txt | |
| parent | f2d84b3ebdffec025513ed4057704ed3d2177cfe (diff) | |
Look for csdp in $PATH at runtime, remove -csdpdir configure option
The csdp path computed by the configure script wasn't used at all, but
was forcing presence of csdp at configure time whereas it is not used
at all in the build process. Instead, we replace the configure-time
check with a runtime check for existence of csdp in $PATH.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc/debugging.txt')
0 files changed, 0 insertions, 0 deletions