From 328cd1cb92e463b2a9cdd669e7e31090dc905c64 Mon Sep 17 00:00:00 2001 From: glondu Date: Sun, 11 Apr 2010 16:58:12 +0000 Subject: 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 --- lib/system.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index 2932d7b669..cc55f4d66b 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -66,6 +66,8 @@ val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a val run_command : (string -> string) -> (string -> unit) -> string -> Unix.process_status * string +val search_exe_in_path : string -> string option + (*s Time stamps. *) type time -- cgit v1.2.3