diff options
| author | Enrico Tassi | 2019-05-24 15:48:04 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-24 15:48:04 +0200 |
| commit | 5596cf352d1c265fd5627dc19416d2b55c10f2b7 (patch) | |
| tree | d00e6dcca11f57903a4a72db1d2ae76017cadebc | |
| parent | 831639deec0ce88fca4ede4756815cf434088ac3 (diff) | |
| parent | 2ba0994e11b3cebf4d33c5712f873998ad5ddd7b (diff) | |
Merge PR #10209: Fix #10208 don't fail when passed extensionless -topfile
Reviewed-by: ppedrot
| -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 660dc27211..3b5323a3b8 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2698,8 +2698,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 |