aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2018-05-22 10:30:51 +0200
committerThéo Zimmermann2018-05-22 10:30:51 +0200
commit61e088161858fa7e6ff494cadd7362b9deccd438 (patch)
treea88bf6867103dbf87d701cc2e2205e67b5f4e7d0 /lib/system.ml
parentd6eb4a26648817f6b034e95c02622cadf0fa65ca (diff)
parentdb1719fbac08b5582fafddd4b76ef92f69cc5bc1 (diff)
Merge PR #6859: [stm] Make toplevels standalone executables.
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml18
1 files changed, 6 insertions, 12 deletions
diff --git a/lib/system.ml b/lib/system.ml
index dfede29e8f..f109c71925 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -116,18 +116,6 @@ let where_in_path ?(warn=true) path filename =
let f = Filename.concat lpe filename in
if file_exists_respecting_case lpe filename then [lpe,f] else []))
-let where_in_path_rex path rex =
- search path (fun lpe ->
- try
- let files = Sys.readdir lpe in
- CList.map_filter (fun name ->
- try
- ignore(Str.search_forward rex name 0);
- Some (lpe,Filename.concat lpe name)
- with Not_found -> None)
- (Array.to_list files)
- with Sys_error _ -> [])
-
let find_file_in_path ?(warn=true) paths filename =
if not (Filename.is_implicit filename) then
(* the name is considered to be a physical name and we use the file
@@ -312,3 +300,9 @@ let with_time ~batch f x =
let msg2 = if batch then "" else " (failure)" in
Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
+
+let get_toplevel_path top =
+ let dir = Filename.dirname Sys.argv.(0) in
+ let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
+ let eff = if Dynlink.is_native then ".opt" else ".byte" in
+ dir ^ Filename.dir_sep ^ top ^ eff ^ exe