From 37ab4ffd30ea794a9769cebd33cf954f6c2e8070 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 19 Jun 2016 01:26:16 +0200
Subject: Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.

---
 toplevel/vernac.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'toplevel')

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);
-- 
cgit v1.2.3