From c62a286bad2ec0ced1e7b5e8987f5f7e476ab11c Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Tue, 22 Aug 2017 15:38:06 -0400 Subject: use OCaml 4.03-compatible Filename functions --- pretyping/nativenorm.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'pretyping/nativenorm.ml') diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 9ca632f4b..39c2ceeba 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -54,8 +54,17 @@ let get_available_profile_filename () = let profile_filename = get_profile_filename () in let dir = Filename.dirname profile_filename in let base = Filename.basename profile_filename in - let ext = Filename.extension base in - let name = Filename.remove_extension base in + (* starting with OCaml 4.04, could use Filename.remove_extension and Filename.extension, which + gets rid of need for exception-handling here + *) + let (name,ext) = + try + let nm = Filename.chop_extension base in + let nm_len = String.length nm in + let ex = String.sub base nm_len (String.length base - nm_len) in + (nm,ex) + with Invalid_argument _ -> (base,"") + in try (* unlikely race: fn deleted, another process uses fn *) Filename.temp_file ~temp_dir:dir (name ^ "_") ext -- cgit v1.2.3