Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.

1 files changed, 4 insertions, 1 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 94972e272..9c3b170b9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -300,9 +300,12 @@ let ensure_ext ext f =
     f ^ ext
   end
 
+let chop_extension f =
+  try Filename.chop_extension f with _ -> f
+
 let ensure_bname src tgt =
   let src, tgt = Filename.basename src, Filename.basename tgt in
-  let src, tgt = Filename.chop_extension src, Filename.chop_extension tgt in
+  let src, tgt = chop_extension src, chop_extension tgt in
   if src <> tgt then begin
     Feedback.msg_error (str "Source and target file names must coincide, directories can differ");
     Feedback.msg_error (str "Source: " ++ str src);