aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorglondu2010-04-11 16:58:12 +0000
committerglondu2010-04-11 16:58:12 +0000
commit328cd1cb92e463b2a9cdd669e7e31090dc905c64 (patch)
tree96efe136562782c27692ed1aa1ff89899c8b9792 /lib/system.ml
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 'lib/system.ml')
-rw-r--r--lib/system.ml20
1 files changed, 20 insertions, 0 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 4afae39188..4b657e4855 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