From 1cdb96f0201b4dda6bdb5f326f60314ae9bf700b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 9 Jun 2016 11:35:02 +0200
Subject: Remove failure on non-.v files (bug #4752).

The error message was not only causing coqtop to exit, but also coqide to
crash, which led to a rather poor user experience. Since the code does not
actually care about the file extension, this commit just removes the test.
---
 ide/ide_slave.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 2e6a361c66..1f933fb8a5 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -351,8 +351,6 @@ let init =
      match file with
      | None -> Stm.get_current_state ()
      | Some file ->
-         if not (Filename.check_suffix file ".v") then
-           error "A file with suffix .v is expected.";
          let dir = Filename.dirname file in
          let open Loadpath in let open CUnix in
          let initial_id, _ =
-- 
cgit v1.2.3