From 2ba0994e11b3cebf4d33c5712f873998ad5ddd7b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 22 May 2019 13:52:13 +0200
Subject: Fix #10208 don't fail when passed extensionless -topfile

---
 stm/stm.ml | 4 ++--
 1 file 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
 
-- 
cgit v1.2.3