diff options
Diffstat (limited to 'utils/misc.ml')
| -rw-r--r-- | utils/misc.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/utils/misc.ml b/utils/misc.ml index 4841b7183..71998ac0d 100644 --- a/utils/misc.ml +++ b/utils/misc.ml @@ -75,6 +75,18 @@ let find_in_path path name = in try_dir path end +let find_in_path_uncap path name = + let uname = String.uncapitalize name in + let rec try_dir = function + [] -> raise Not_found + | dir::rem -> + let fullname = Filename.concat dir name in + let ufullname = Filename.concat dir uname in + if Sys.file_exists fullname then fullname + else if Sys.file_exists ufullname then ufullname + else try_dir rem + in try_dir path + let remove_file filename = try Sys.remove filename |