diff options
Diffstat (limited to 'utils/misc.ml')
| -rw-r--r-- | utils/misc.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/utils/misc.ml b/utils/misc.ml index e142ce2ad2..989c313bb2 100644 --- a/utils/misc.ml +++ b/utils/misc.ml @@ -154,10 +154,7 @@ let no_overflow_lsl a = min_int asr 1 <= a && a <= max_int asr 1 (* String operations *) let chop_extension_if_any fname = - try - ignore(String.index (Filename.basename fname) '.'); - Filename.chop_extension fname - with Not_found -> fname + try Filename.chop_extension fname with Invalid_argument _ -> fname let search_substring pat str start = let rec search i j = |