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

2 files changed, 22 insertions, 0 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 4afae3918..4b657e485 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -284,6 +284,26 @@ let run_command converter f c =
   done;
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
+let path_separator = if Sys.os_type = "Unix" then ':' else ';'
+
+let search_exe_in_path exe =
+  try
+    let path = Sys.getenv "PATH" in
+    let n = String.length path in
+    let rec aux i =
+      if i < n then
+        let j =
+          try String.index_from path i path_separator
+          with Not_found -> n
+        in
+        let dir = String.sub path i (j-i) in
+        let exe = Filename.concat dir exe in
+        if Sys.file_exists exe then Some exe else aux (i+1)
+      else
+        None
+    in aux 0
+  with Not_found -> None
+
 (* Time stamps. *)
 
 type time = float * float * float
diff --git a/lib/system.mli b/lib/system.mli
index 2932d7b66..cc55f4d66 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