aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-11 16:58:12 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-11 16:58:12 +0000
commit328cd1cb92e463b2a9cdd669e7e31090dc905c64 (patch)
tree96efe136562782c27692ed1aa1ff89899c8b9792 /config
parentf2d84b3ebdffec025513ed4057704ed3d2177cfe (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 'config')
-rw-r--r--config/coq_config.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 5feb96303..2cd1e4543 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -55,8 +55,6 @@ val plugins_dirs : string list
val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
-val csdp : string option (* the path to CSDP, for the Micromega plugin *)
-
val browser : string
(** default web browser to use, may be overriden by environment
variable COQREMOTEBROWSER *)