diff options
| -rw-r--r-- | ide/coqide.ml | 5 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index ba20c771a6..c96a34018a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1328,10 +1328,7 @@ let build_ui () = (** {2 Coqide main function } *) let make_file_buffer f = - let f = - if Sys.file_exists f || Filename.check_suffix f ".v" then f - else f^".v" - in + let f = if Filename.check_suffix f ".v" then f else f^".v" in FileAux.load_file ~maycreate:true f let make_scratch_buffer () = diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 59d9078bb8..62e1bad431 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -345,6 +345,8 @@ 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, _ = |