2 files changed, 22 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
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