diff options
| author | Gaëtan Gilbert | 2019-05-22 13:52:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-22 13:52:13 +0200 |
| commit | 2ba0994e11b3cebf4d33c5712f873998ad5ddd7b (patch) | |
| tree | 8306ea1dc70d7ce9360e28715866f7772d97dee0 /stm | |
| parent | e7d03413c6b8f8fbcc537a43da4c3f9ff19007ad (diff) | |
Fix #10208 don't fail when passed extensionless -topfile
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 6f7cefb582..c8278fee73 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2693,8 +2693,8 @@ let dirpath_of_file f = Loadpath.logical lp with Not_found -> Libnames.default_root_prefix in - let file = Filename.chop_extension (Filename.basename f) in - let id = Id.of_string file in + let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in + let id = Id.of_string f in let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir |