From 3e6fa1cbdc0ec145728089000595b6ea29f37a4c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Nov 2016 16:35:56 +0100
Subject: Fix #5183 - Two CoqIDE crash errors

When opening a file without extension, an uncaught exception was
occurring.

Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
---
 lib/aux_file.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/aux_file.ml')

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c6c7b42429..0f0f09aa23 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -17,6 +17,10 @@ let version = 1
 
 let oc = ref None
 
+let chop_extension f =
+  if check_suffix f ".v" then chop_extension f
+  else f
+
 let aux_file_name_for vfile =
   dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
 
-- 
cgit v1.2.3